aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr.ml2
-rw-r--r--interp/constrexpr_ops.ml2
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml2
-rw-r--r--parsing/g_constr.mlg2
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/proof_diffs.ml6
-rw-r--r--user-contrib/Ltac2/tac2quote.ml2
13 files changed, 20 insertions, 20 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) ->
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index df2de3333d..931ffccb27 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -263,7 +263,7 @@ GRAMMAR EXTEND Gram
| "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
| "?"; "["; id = identref; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id.CAst.v, None) }
| "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) }
- | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
+ | id = pattern_identref; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
;
inst:
[ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ]
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 503035c6c3..c5df5d7968 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t =
(* Meta in constr are not user-parsable and are mapped to Evar *)
if n = Constr_matching.special_meta then
(* Using a dash to be unparsable *)
- GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+ GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", [])
else
- GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
+ GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), [])
| Var id ->
(* Discriminate between section variable and non-section variable *)
(try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None)
@@ -793,7 +793,7 @@ and detype_r d flags avoid env sigma t =
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
(List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl)
in
- GEvar (id,
+ GEvar (CAst.make id,
List.map (on_snd (detype d flags avoid env sigma)) l)
| Ind (ind_sp,u) ->
GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index fd6083abd1..dc5fd80f9e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
Option.equal (List.equal glob_level_eq) u1 u2
| GVar id1, GVar id2 -> Id.equal id1 id2
| GEvar (id1, arg1), GEvar (id2, arg2) ->
- Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
+ Id.equal id1.CAst.v id2.CAst.v && List.equal (instance_eq f) arg1 arg2
| GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
| GApp (f1, arg1), GApp (f2, arg2) ->
f f1 f2 && List.equal f arg1 arg2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 04e9382015..a49c8abe26 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -75,7 +75,7 @@ type 'a glob_constr_r =
| GVar of Id.t
(** An identifier that cannot be regarded as "GRef".
Bound variables are typically represented this way. *)
- | GEvar of existential_name * (lident * 'a glob_constr_g) list
+ | GEvar of existential_name CAst.t * (lident * 'a glob_constr_g) list
| GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
| GApp of 'a glob_constr_g * 'a glob_constr_g list
| GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9c400da4ae..f79c4f4e96 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -493,7 +493,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> ty
type pretyper = {
pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
- pretype_evar : pretyper -> existential_name * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
@@ -628,13 +628,13 @@ struct
let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
- let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
+ let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
let id = interp_ltac_id env id in
let evk =
try Evd.evar_key id sigma
- with Not_found -> error_evar_not_found ?loc !!env sigma id in
+ with Not_found -> error_evar_not_found ?loc:locid !!env sigma id in
let hyps = evar_filtered_context (Evd.find sigma evk) in
let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c4f0f18e27..7bb4a6e273 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev
type pretyper = {
pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
- pretype_evar : pretyper -> existential_name * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 30335d9826..4200268acc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -227,7 +227,7 @@ let tag_var = tag Tag.variable
let pr_evar pr id l =
hov 0 (
- tag_evar (str "?" ++ pr_id id) ++
+ tag_evar (str "?" ++ pr_lident id) ++
(match l with
| [] -> mt()
| l ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 43f70dfecc..fab44e8875 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -511,12 +511,12 @@ let match_goals ot nt =
| CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
| CPatVar _, CPatVar _ -> ()
| CEvar (n,l), CEvar (n2,l2) ->
- let oevar = if ogname = "" then Id.to_string n else ogname in
- nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar;
+ let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in
+ nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar;
iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2
| CEvar (n,l), nt' ->
(* pass down the old goal evar name *)
- match_goals_r (Id.to_string n) nt' nt'
+ match_goals_r (Id.to_string n.CAst.v) nt' nt'
| CSort s, CSort s2 -> ()
| CCast (c,c'), CCast (c2,c'2) ->
constr_expr ogname c c2;
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index b346b3ee5c..90f8008dc2 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -229,7 +229,7 @@ let check_pattern_id ?loc id =
let pattern_vars pat =
let rec aux () accu pat = match pat.CAst.v with
| Constrexpr.CPatVar id
- | Constrexpr.CEvar (id, []) ->
+ | Constrexpr.CEvar ({CAst.v=id}, []) ->
let loc = pat.CAst.loc in
let () = check_pattern_id ?loc id in
Id.Map.add id loc accu
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:01:00 +0000