aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/pretyping.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5ad06a6e52..0a3f6d995a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -21,7 +21,7 @@ open Pp
(* Metavariables *)
type patvar_map = (patvar * constr) list
-let patvar_of_int n = Names.id_of_string (string_of_int n)
+let patvar_of_int n = Names.id_of_string ("X" ^ string_of_int n)
let pr_patvar = pr_id
(* Patterns *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f94c14e71f..0e76558f1f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -228,7 +228,7 @@ let rec pretype tycon env isevars lvar lmeta = function
assert (not someta);
let j =
try
- List.assoc n lmeta
+ List.assoc n (lmeta@lvar)
with
Not_found ->
user_err_loc