0001630: Make identifiers in Coq proofs more similar to those from C code

Notes
(0004491) correnson (manager) 2014-02-05 13:13	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 "<ident>_<number>" is reserved for local variables, whereas "<ident>" might clash with keywords, models and (unknown) user definitions.

(0004492) correnson (manager) 2014-02-05 13:15	Feature wish postponed to a future release.

(0004971) jens (reporter) 2014-03-16 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 Coq-level.

(0005189) correnson (manager) 2014-06-02 17:05 edited on: 2014-06-02 17:06	Fix committed to master branch. Only for short names (1 letter) with index 0.

Relationships