aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 90a3728ebb..05af1652e1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -92,7 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with
let rec pattern_of_constr t =
match kind_of_term t with
| Rel n -> PRel n
- | Meta n -> PMeta (Some (id_of_string (string_of_int n)))
+ | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
| Var id -> PVar id
| Sort (Prop c) -> PSort (RProp c)
| Sort (Type _) -> PSort (RType None)