
This is difficult to implement in a safe way. We need to avoid name clashes, and we rely on patterns to do this. Hence, pattern "_" is reserved for local variables, whereas "" might clash with keywords, models and (unknown) user definitions. 

(0004971)

jens

20140316 18:32


Could this be done at least for the names in logic declarations in ACSL?
For example, the variable names of an axiom such as
axiom CountUnion:
\forall value_type *a, v, integer i, j, k;
0 <= i <= j <= k ==> Count(a, v, i ,k) == Count(a, v, i, j) + Count(a, v, j, k);
looks like this on the Coq level
Q_CountUnion :
forall (i_0 j_0 k_0 v_0 : int) (Mint_0 : farray addr int) (a_0 : addr),
0 <= i_0 >
i_0 <= j_0 >
j_0 <= k_0 >
is_sint32 v_0 >
L_Count Mint_0 a_0 v_0 i_0 k_0 =
L_Count Mint_0 a_0 v_0 i_0 j_0 + L_Count Mint_0 a_0 v_0 j_0 k_0
It would be nice, if the arguments would read i, j, k, v, and a on the Coqlevel. 
