aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml6
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml7
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation_ops.ml39
-rw-r--r--interp/ppextend.ml2
-rw-r--r--interp/ppextend.mli2
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli2
12 files changed, 42 insertions, 38 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d0a19b9a6..771c137344 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -320,13 +320,13 @@ let coerce_reference_to_id = function
(str "This expression should be a simple identifier.")
let coerce_to_id = function
- | { CAst.v = CRef (Ident (loc,id),_); _ } -> (loc,id)
+ | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id)
| { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
- | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id)
- | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous)
+ | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id)
+ | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous)
| { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
(str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f5eff693ff..f1bee65ef8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1087,7 +1087,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* Not "goal_concl_style" means do alpha-conversion avoiding only *)
(* those goal/section/rel variables that occurs in the subterm under *)
(* consideration; see namegen.ml for further details *)
- let avoid = if goal_concl_style then ids_of_context env else [] in
+ let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
extern false (scopt,[]) vars r
@@ -1099,14 +1099,14 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
extern_constr_gen lax goal_concl_style None env sigma t
let extern_type goal_concl_style env sigma t =
- let avoid = if goal_concl_style then ids_of_context env else [] in
+ let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
extern_glob_type (vars_of_env env) r
let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
let extern_closed_glob ?lax goal_concl_style env sigma t =
- let avoid = if goal_concl_style then ids_of_context env else [] in
+ let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r =
Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
in
@@ -1177,15 +1177,15 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+ | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
let extern_rel_context where env sigma sign =
- let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in
+ let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl) a in
pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6f7c6c8277..1cea307d76 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -469,8 +469,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
| _ -> assert false
in
let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
- let ienv = Id.Set.elements env.ids in
- let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+ let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in
let na = (loc, Name id) in
let bk = Default Explicit in
let _, bl' = intern_assumption intern lvar env [na] bk tyc in
@@ -1939,13 +1938,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| _ ->
let fresh =
Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
- canonize_args t tt (fresh::forbidden_names)
+ canonize_args t tt (Id.Set.add fresh forbidden_names)
((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
end
| _ -> assert false in
let _,args_rel =
List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
- canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
+ canonize_args args_rel l forbidden_names_for_gen [] [] in
match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
| None ->
[], None in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 054e43e7c8..afcd7a2ed2 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -37,7 +37,7 @@ val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
val dump_constraint :
- Constrexpr.typeclass_constraint -> bool -> string -> unit
+ Vernacexpr.typeclass_constraint -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8241c0443..09a0ba83ca 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
in
match kind_of_term (whd_all env t) with
| Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all [] na ([],b) in
+ let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
!rigid, Array.to_list v
| _ -> true, []
diff --git a/interp/notation.ml b/interp/notation.ml
index 176ac3bf68..d3cac1e3e9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -425,7 +425,7 @@ let warn_notation_overridden =
CWarnings.create ~name:"notation-overridden" ~category:"parsing"
(fun (ntn,which_scope) ->
str "Notation" ++ spc () ++ str ntn ++ spc ()
- ++ strbrk "was already used" ++ which_scope)
+ ++ strbrk "was already used" ++ which_scope ++ str ".")
let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0341167318..0967d21f01 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -297,28 +297,29 @@ let compare_recursive_parts found f f' (iterator,subc) =
user_err ?loc:(subtract_loc loc1 loc2)
(str "Both ends of the recursive pattern are the same.")
| Some (x,y,RecursiveTerms lassoc) ->
- let newfound,x,y,lassoc =
+ let toadd,x,y,lassoc =
if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
then
- !found,x,y,lassoc
+ None,x,y,lassoc
else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
then
- !found,y,x,not lassoc
+ None,y,x,not lassoc
else
- (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
+ Some (x,y),x,y,lassoc in
let iterator =
f' (if lassoc then iterator
else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
- (* found have been collected by compare_constr *)
- found := newfound;
+ (* found variables have been collected by compare_constr *)
+ found := (List.remove Id.equal y (pi1 !found),
+ Option.fold_right (fun a l -> a::l) toadd (pi2 !found),
+ pi3 !found);
NList (x,y,iterator,f (Option.get !terminator),lassoc)
| Some (x,y,RecursiveBinders (t_x,t_y)) ->
- let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
(* found have been collected by compare_constr *)
- found := newfound;
+ found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found);
check_is_hole x t_x;
check_is_hole y t_y;
NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -348,7 +349,7 @@ let notation_constr_and_vars_of_glob_constr a =
| _c ->
aux' c
and aux' x = DAst.with_val (function
- | GVar id -> add_id found id; NVar id
+ | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
| GApp (g,args) -> NApp (aux g, List.map aux args)
| GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
| GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
@@ -576,7 +577,7 @@ let rec subst_notation_constr subst bound raw =
if r1' == r1 && k' == k then raw else NCast(r1',k')
let subst_interpretation subst (metas,pat) =
- let bound = List.map fst metas in
+ let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
(**********************************************************************)
@@ -823,7 +824,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
alp, b :: bl
| _ -> raise No_match in
let alp, bl = unify alp bl bl' in
- let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
alp, add_bindinglist_env sigma var bl
with Not_found ->
alp, add_bindinglist_env sigma var bl
@@ -909,7 +910,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc
| GLambda (na,bk,t,b) as b0 ->
begin match na, DAst.get b with
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
- when islambda && is_gvar p e ->
+ when islambda && is_gvar p e && not (occur_glob_constr p b) ->
match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
| _, _ when islambda ->
match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
@@ -918,7 +919,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc
| GProd (na,bk,t,b) as b0 ->
begin match na, DAst.get b with
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
- when not islambda && is_gvar p e ->
+ when not islambda && is_gvar p e && not (occur_glob_constr p b) ->
match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
| Name _, _ when not islambda ->
match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
@@ -991,8 +992,6 @@ let does_not_come_from_already_eta_expanded_var glob =
(* checked). *)
match DAst.get glob with GVar _ -> false | _ -> true
-let is_var c = match DAst.get c with GVar _ -> true | _ -> false
-
let rec match_ inner u alp metas sigma a1 a2 =
let open CAst in
let loc = a1.loc in
@@ -1009,7 +1008,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
begin match na1, DAst.get b1, iter with
(* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
- | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e ->
+ | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _)
+ when is_gvar p e && not (occur_glob_constr p b1) ->
let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
@@ -1027,7 +1027,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
(* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
begin match na1, DAst.get b1, iter, termin with
- | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e ->
+ | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _
+ when is_gvar p e && not (occur_glob_constr p b1) ->
let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
@@ -1049,7 +1050,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
begin match na1, DAst.get b1, na2 with
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
- when is_var e && is_bindinglist_meta id metas ->
+ when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
match_in u alp metas sigma b1 b2
| _, _, Name id when is_bindinglist_meta id metas ->
@@ -1142,7 +1143,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
| _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
let avoid =
- free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
+ Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
let id' = Namegen.next_ident_away id avoid in
let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
let sigma = match t2 with
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 3ebc9b71d2..ce19dd8a92 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -36,5 +36,5 @@ type unparsing =
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpBinderListMetaVar of int * bool * unparsing list
| UnpTerminal of string
- | UnpBox of ppbox * unparsing list
+ | UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 6ff5a42728..7b62a2074b 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -29,5 +29,5 @@ type unparsing =
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpBinderListMetaVar of int * bool * unparsing list
| UnpTerminal of string
- | UnpBox of ppbox * unparsing list
+ | UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a1e5bd0ea9..dc0f60dcf2 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -110,7 +110,7 @@ let revert_reserved_type t =
let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
let filter _ pat =
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 274ea6213b..45dec5112b 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -50,6 +50,8 @@ let wit_ref = make0 "ref"
let wit_quant_hyp = make0 "quant_hyp"
+let wit_sort_family = make0 "sort_family"
+
let wit_constr =
make0 "constr"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 1d4a29b9c2..dffbd6659f 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -47,6 +47,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+val wit_sort_family : (Sorts.family, unit, unit) genarg_type
+
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:39:49 +0000