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.ml2
-rw-r--r--parsing/g_constr.mlg6
-rw-r--r--pretyping/detyping.ml4
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--printing/ppconstr.ml2
10 files changed, 18 insertions, 18 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index c98e05370e..bfdee7c50d 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 * (Id.t * constr_expr) list
+ | CEvar of Glob_term.existential_name * (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 ce8e7d3c2c..3400485ad5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
List.equal (List.equal local_binder_eq) bl1 bl2
and instance_eq (x1,c1) (x2,c2) =
- Id.equal x1 x2 && constr_expr_eq c1 c2
+ Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2
and cast_expr_eq c1 c2 = match c1, c2 with
| CastConv t1, CastConv t2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 43fef8685d..a609dd66c3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -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 (on_snd (glob_of_pat avoid env sigma)) l)
+ GEvar (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/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 1ec83c496a..df2de3333d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram
| "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
;
appl_arg:
- [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+ [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
| c=operconstr LEVEL "9" -> { (c,None) } ] ]
;
atomic_constr:
@@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram
| n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
| s = string -> { CAst.make ~loc @@ CPrim (String s) }
| "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
- | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, 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) } ] ]
;
inst:
- [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ]
+ [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ]
;
evar_instance:
[ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7fcb0795bd..503035c6c3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -788,10 +788,10 @@ and detype_r d flags avoid env sigma t =
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
- id,l
+ id,List.map (fun (id,c) -> (CAst.make id,c)) l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
- (List.map (fun c -> (Id.of_string "__",c)) cl)
+ (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl)
in
GEvar (id,
List.map (on_snd (detype d flags avoid env sigma)) l)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5bd26be823..fd6083abd1 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with
| (GFix _ | GCoFix _), _ -> false
let instance_eq f (x1,c1) (x2,c2) =
- Id.equal x1 x2 && f c1 c2
+ Id.equal x1.CAst.v x2.CAst.v && f c1 c2
let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
| GRef (gr1, u1), GRef (gr2, u2) ->
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 526eac6f1e..04e9382015 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 * (Id.t * 'a glob_constr_g) list
+ | GEvar of existential_name * (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 b9825b6a92..9c400da4ae 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -365,9 +365,9 @@ let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = functio
| Some t ->
Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
-let check_instance loc subst = function
+let check_instance subst = function
| [] -> ()
- | (id,_) :: _ ->
+ | (CAst.{loc;v=id},_) :: _ ->
if List.mem_assoc id subst then
user_err ?loc (Id.print id ++ str "appears more than once.")
else
@@ -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 * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name * (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;
@@ -587,10 +587,10 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
strbrk " is not well-typed.") in
let sigma, c, update =
try
- let c = List.assoc id update in
+ let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in
let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in
check_body sigma id (Some c.uj_val);
- sigma, c.uj_val, List.remove_assoc id update
+ sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update
with Not_found ->
try
let (n,b',t') = lookup_rel_id id (rel_context !!env) in
@@ -609,7 +609,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
str " in current context: no binding for " ++ Id.print id ++ str ".") in
((id,c)::subst, update, sigma) in
let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
- check_instance loc subst inst;
+ check_instance subst inst;
sigma, List.map snd subst
module Default =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c03374c59f..c4f0f18e27 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 * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name * (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 267f5e0b5f..30335d9826 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -231,7 +231,7 @@ let tag_var = tag Tag.variable
(match l with
| [] -> mt()
| l ->
- let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
+ let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in
str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
let las = lapp
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:55:36 +0000