diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 2 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 2 | ||||
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index bfdee7c50d..d14d156ffc 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -108,7 +108,7 @@ and constr_expr_r = * constr_expr * constr_expr | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar - | CEvar of Glob_term.existential_name * (lident * constr_expr) list + | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3400485ad5..7075d082ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -156,7 +156,7 @@ let rec constr_expr_eq e1 e2 = | CPatVar i1, CPatVar i2 -> Id.equal i1 i2 | CEvar (id1, c1), CEvar (id2, c2) -> - Id.equal id1 id2 && List.equal instance_eq c1 c2 + Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a609dd66c3..88350fbda5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -978,7 +978,7 @@ let rec extern inctx ?impargs scopes vars r = if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n - | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) + | Evar_kinds.FirstOrderPatVar n -> CEvar (CAst.make n,[])) | GApp (f,args) -> (match DAst.get f with @@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l) + GEvar (CAst.make id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 48fb4a4a5d..959b61a3d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2188,7 +2188,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> DAst.make ?loc @@ - GPatVar (Evar_kinds.FirstOrderPatVar n) + GPatVar (Evar_kinds.FirstOrderPatVar n.CAst.v) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> |