diff options
| -rw-r--r-- | contrib/correctness/pmisc.ml | 4 | ||||
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index ca7cee2e2e..ba96b98b71 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -110,7 +110,7 @@ let reset_names,pre_name,post_name,inv_name, (fun () -> next "for" forr Anonymous), (fun () -> string_of_id (next "Label" label Anonymous)) -let default = id_of_string "_" +let default = id_of_string "x_" let id_of_name = function Name id -> id | Anonymous -> default @@ -169,7 +169,7 @@ let coq_true = mkConstruct ((bool_sp,0),1) let coq_false = mkConstruct ((bool_sp,0),2) let constant s = - let id = id_of_string s in + let id = Constrextern.id_of_v7_string s in Termops.global_reference id let connective_and = id_of_string "prog_bool_and" diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index eab548215f..221445b58d 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -103,7 +103,7 @@ open Util open Coqast let mk_id loc id = mkRefC (Ident (loc, id)) -let mk_ref loc s = mk_id loc (id_of_string s) +let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s) let mk_appl loc1 loc2 f args = CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args) |