aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml17
-rw-r--r--pretyping/cbv.mli1
-rw-r--r--pretyping/classops.ml3
-rw-r--r--pretyping/classops.mli1
-rw-r--r--pretyping/coercion.ml5
-rw-r--r--pretyping/coercion.mli1
-rw-r--r--pretyping/constr_matching.ml80
-rw-r--r--pretyping/detyping.ml10
-rw-r--r--pretyping/evarconv.ml1
-rw-r--r--pretyping/evarconv.mli1
-rw-r--r--pretyping/evardefine.ml1
-rw-r--r--pretyping/evarsolve.ml1
-rw-r--r--pretyping/find_subterm.mli1
-rw-r--r--pretyping/inductiveops.ml1
-rw-r--r--pretyping/miscops.ml2
-rw-r--r--pretyping/patternops.ml5
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--pretyping/pretype_errors.ml1
-rw-r--r--pretyping/pretyping.ml105
-rw-r--r--pretyping/program.ml1
-rw-r--r--pretyping/reductionops.ml12
-rw-r--r--pretyping/reductionops.mli5
-rw-r--r--pretyping/tacred.mli1
-rw-r--r--pretyping/typeclasses_errors.ml1
-rw-r--r--pretyping/typeclasses_errors.mli1
-rw-r--r--pretyping/typing.ml3
-rw-r--r--pretyping/unification.ml5
27 files changed, 152 insertions, 115 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c5cf74ccfb..6bc2a4f94b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -563,31 +563,30 @@ let dependencies_in_rhs sigma nargs current tms eqns =
declarations [d(i+1);...;dn] the term [tmi] is dependent in.
[find_dependencies_signature (used1,...,usedn) ((tm1,d1),...,(tmn,dn))]
- returns [(deps1,...,depsn)] where [depsi] is a subset of n,..,i+1
+ returns [(deps1,...,depsn)] where [depsi] is a subset of tm(i+1),..,tmn
denoting in which of the d(i+1)...dn, the term tmi is dependent.
- Dependencies are expressed by index, e.g. in dependency list
- [n-2;1], [1] points to [dn] and [n-2] to [d3]
*)
let rec find_dependency_list sigma tmblock = function
| [] -> []
- | (used,tdeps,d)::rest ->
+ | (used,tdeps,tm,d)::rest ->
let deps = find_dependency_list sigma tmblock rest in
if used && List.exists (fun x -> dependent_decl sigma x d) tmblock
then
- List.add_set Int.equal
- (List.length rest + 1) (List.union Int.equal deps tdeps)
+ match EConstr.kind sigma tm with
+ | Rel n -> List.add_set Int.equal n (List.union Int.equal deps tdeps)
+ | _ -> List.union Int.equal deps tdeps
else deps
let find_dependencies sigma is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
let deps = find_dependency_list sigma (tm::tmtypleaves) nextlist in
if is_dep_or_cstr_in_rhs || not (List.is_empty deps)
- then ((true ,deps,d)::nextlist)
- else ((false,[] ,d)::nextlist)
+ then ((true ,deps,tm,d)::nextlist)
+ else ((false,[] ,tm,d)::nextlist)
let find_dependencies_signature sigma deps_in_rhs typs =
let l = List.fold_right2 (find_dependencies sigma) deps_in_rhs typs [] in
- List.map (fun (_,deps,_) -> deps) l
+ List.map (fun (_,deps,_,_) -> deps) l
(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
and xn:Tn has just been regeneralized into x:Tn so that the terms
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index b014af2c7f..eb25994bef 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open EConstr
open Environ
open CClosure
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 632ba0d9cd..32da81f96c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
open Environ
open Libobject
open Term
-open Termops
open Mod_subst
(* usage qque peu general: utilise aussi dans record *)
@@ -388,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
old_inheritance_graph
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
- if is_ambig && is_verbose () then
+ if is_ambig && not !quiet then
Feedback.msg_info (message_ambig !ambig_paths)
type coercion = {
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0d741a5a5d..c4238e8b0d 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Environ
open EConstr
open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdfa..e6c0075c5b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,7 +22,6 @@ open Environ
open EConstr
open Vars
open Reductionops
-open Typeops
open Pretype_errors
open Classops
open Evarutil
@@ -479,8 +478,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
(* We eta-expand (hence possibly modifying the original term!) *)
(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
(* has type forall (x:u1), u2 (with v' recursively obtained) *)
- (* Note: we retype the term because sort-polymorphism may have *)
- (* weaken its type *)
+ (* Note: we retype the term because template polymorphism may have *)
+ (* weakened its type *)
let name = match name with
| Anonymous -> Name Namegen.default_dependent_ident
| _ -> name in
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index bc63d092d9..ea3d3f0fa1 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -8,7 +8,6 @@
open Evd
open Names
-open Term
open Environ
open EConstr
open Glob_term
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index efe03bc2e9..2334be9664 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -83,32 +83,70 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
let rec build_lambda sigma vars ctx m = match vars with
| [] ->
- let len = List.length ctx in
- EConstr.Vars.lift (-1 * len) m
+ if Vars.closed0 sigma m then m else raise PatternMatchingFailure
| n :: vars ->
- let open EConstr in
(* change [ x1 ... xn y z1 ... zm |- t ] into
[ x1 ... xn z1 ... zm |- lam y. t ] *)
- let len = List.length ctx in
- let init i =
- if i < pred n then mkRel (i + 2)
- else if Int.equal i (pred n) then mkRel 1
- else mkRel (i + 1)
- in
- let m = Vars.substl (List.init len init) m in
let pre, suf = List.chop (pred n) ctx in
- match suf with
+ let (na, t, suf) = match suf with
| [] -> assert false
- | (_, na, t) :: suf ->
- let map i = if i > n then pred i else i in
- let vars = List.map map vars in
- (** Check that the abstraction is legal *)
- let frels = free_rels sigma t in
- let brels = List.fold_right Int.Set.add vars Int.Set.empty in
- let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
- (** Create the abstraction *)
- let m = mkLambda (na, t, m) in
- build_lambda sigma vars (pre @ suf) m
+ | (_, na, t) :: suf -> (na, t, suf)
+ in
+ (** Check that the abstraction is legal by generating a transitive closure of
+ its dependencies. *)
+ let is_nondep t clear = match clear with
+ | [] -> true
+ | _ ->
+ let rels = free_rels sigma t in
+ let check i b = b || not (Int.Set.mem i rels) in
+ List.for_all_i check 1 clear
+ in
+ let fold (_, _, t) clear = is_nondep t clear :: clear in
+ (** Produce a list of booleans: true iff we keep the hypothesis *)
+ let clear = List.fold_right fold pre [false] in
+ let clear = List.drop_last clear in
+ (** If the conclusion depends on a variable we cleared, failure *)
+ let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
+ (** Create the abstracted term *)
+ let fold (k, accu) keep =
+ if keep then
+ let k = succ k in
+ (k, Some k :: accu)
+ else (k, None :: accu)
+ in
+ let keep, shift = List.fold_left fold (0, []) clear in
+ let shift = List.rev shift in
+ let map = function
+ | None -> mkProp (** dummy term *)
+ | Some i -> mkRel (i + 1)
+ in
+ (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
+ let subst =
+ List.map map shift @
+ mkRel 1 ::
+ List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
+ in
+ let map i (id, na, c) =
+ let i = succ i in
+ let subst = List.skipn i subst in
+ let subst = List.map (fun c -> Vars.lift (- i) c) subst in
+ (id, na, substl subst c)
+ in
+ let pre = List.mapi map pre in
+ let pre = List.filter_with clear pre in
+ let m = substl subst m in
+ let map i =
+ if i > n then i - n + keep
+ else match List.nth shift (i - 1) with
+ | None ->
+ (** We cleared a variable that we wanted to abstract! *)
+ raise PatternMatchingFailure
+ | Some k -> k
+ in
+ let vars = List.map map vars in
+ (** Create the abstraction *)
+ let m = mkLambda (na, Vars.lift keep t, m) in
+ build_lambda sigma vars (pre @ suf) m
let rec extract_bound_aux k accu frels ctx = match ctx with
| [] -> accu
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba4086795..0d798b4d94 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Term
-open Environ
open EConstr
open Vars
open Inductiveops
@@ -423,7 +422,9 @@ let detype_sort sigma = function
| Type u ->
GType
(if !print_universes
- then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
+ then
+ let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in
+ [dl, Name.mk_name (Id.of_string_soft u)]
else [])
type binder_kind = BProd | BLambda | BLetIn
@@ -435,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
let set_detype_anonymous f = detype_anonymous := f
let detype_level sigma l =
- GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
+ let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in
+ GType (Some (dl, Name.mk_name (Id.of_string_soft l)))
let detype_instance sigma l =
let l = EInstance.kind sigma l in
@@ -696,7 +698,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
let c = detype (lax,false) avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
- let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
+ let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
GLetIn (dl, na', c, t, r)
let detype_rel_context ?(lax=false) where avoid env sigma sign =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4bb66b8e91..305eae15a3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -21,7 +21,6 @@ open Recordops
open Evarutil
open Evardefine
open Evarsolve
-open Globnames
open Evd
open Pretype_errors
open Sigma.Notations
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fc07f0fbea..7cee1e8a7e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open EConstr
open Environ
open Reductionops
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c5ae684e3b..5fd104c781 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,7 +11,6 @@ open Pp
open Names
open Term
open Termops
-open Environ
open EConstr
open Vars
open Namegen
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77086d046c..f0d0114775 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module CVars = Vars
open Util
open CErrors
open Names
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index e3d3b74f10..d22f94e4e5 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Locus
-open Term
open Evd
open Pretype_errors
open Environ
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5b42add285..429e5005ec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
| _ -> raise Not_found
let find_mrectype_vect env sigma c =
- let open EConstr in
let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
match EConstr.kind sigma t with
| Ind ind -> (ind, l)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 7fe81c9a43..1669f8334b 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
let glob_sort_eq g1 g2 = match g1, g2 with
| GProp, GProp -> true
| GSet, GSet -> true
-| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2
| _ -> false
let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 318f94be24..33a68589c1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -20,7 +20,6 @@ open Mod_subst
open Misctypes
open Decl_kinds
open Pattern
-open Evd
open Environ
let case_info_pattern_eq i1 i2 =
@@ -156,7 +155,7 @@ let pattern_of_constr env sigma t =
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
| Proj (p, c) ->
pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
- | Evar (evk,ctxt as ev) ->
+ | Evar (evk,ctxt) ->
(match snd (Evd.evar_source evk sigma) with
| Evar_kinds.MatchingVar (b,id) ->
assert (not b); PMeta (Some id)
@@ -220,6 +219,8 @@ let instantiate_pattern env sigma lvar c =
ctx
in
let c = substl inst c in
+ (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
+ let c = Evarutil.nf_evar sigma c in
pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
with Not_found (* List.index failed *) ->
let vars =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5694d345c1..791fd74ed3 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
open EConstr
open Globnames
open Glob_term
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 24f6d16899..f9cf6b83bc 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Names
open Term
open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a042b73c28..4886423bd0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,7 +33,6 @@ open EConstr
open Vars
open Reductionops
open Type_errors
-open Typeops
open Typing
open Globnames
open Nameops
@@ -193,45 +192,51 @@ let _ =
optwrite = (:=) Universes.set_minimization })
(** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd (loc,s) =
- let names, _ = Global.global_universe_names () in
- if CString.string_contains s "." then
- match List.rev (CString.split '.' s) with
- | [] -> anomaly (str"Invalid universe name " ++ str s)
- | n :: dp ->
- let num = int_of_string n in
- let dp = DirPath.make (List.map Id.of_string dp) in
- let level = Univ.Level.make dp num in
- let evd =
- try Evd.add_global_univ evd level
- with UGraph.AlreadyDeclared -> evd
- in evd, level
- else
- try
- let level = Evd.universe_of_name evd s in
- evd, level
- with Not_found ->
- try
- let id = try Id.of_string s with _ -> raise Not_found in
- evd, snd (Idmap.find id names)
- with Not_found ->
- if not (is_strict_universe_declarations ()) then
- new_univ_level_variable ~loc ~name:s univ_rigid evd
- else user_err ~loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared universe: " ++ str s))
+let interp_universe_level_name ~anon_rigidity evd (loc,s) =
+ match s with
+ | Anonymous ->
+ new_univ_level_variable ~loc anon_rigidity evd
+ | Name s ->
+ let s = Id.to_string s in
+ let names, _ = Global.global_universe_names () in
+ if CString.string_contains ~where:s ~what:"." then
+ match List.rev (CString.split '.' s) with
+ | [] -> anomaly (str"Invalid universe name " ++ str s)
+ | n :: dp ->
+ let num = int_of_string n in
+ let dp = DirPath.make (List.map Id.of_string dp) in
+ let level = Univ.Level.make dp num in
+ let evd =
+ try Evd.add_global_univ evd level
+ with UGraph.AlreadyDeclared -> evd
+ in evd, level
+ else
+ try
+ let level = Evd.universe_of_name evd s in
+ evd, level
+ with Not_found ->
+ try
+ let id = try Id.of_string s with _ -> raise Not_found in
+ evd, snd (Idmap.find id names)
+ with Not_found ->
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ~loc ~name:s univ_rigid evd
+ else user_err ~loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared universe: " ++ str s))
let interp_universe ?loc evd = function
| [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
evd, Univ.Universe.make l
| l ->
List.fold_left (fun (evd, u) l ->
- let evd', l = interp_universe_level_name evd l in
+ (* [univ_flexible_alg] can produce algebraic universes in terms *)
+ let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
(evd', Univ.sup u (Univ.Universe.make l)))
(evd, Univ.Universe.type0m) l
-let interp_universe_level loc evd = function
+let interp_level_info loc evd : Misctypes.level_info -> _ = function
| None -> new_univ_level_variable ~loc univ_rigid evd
- | Some (loc,s) -> interp_universe_level_name evd (loc,s)
+ | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (loc,s)
let interp_sort ?loc evd = function
| GProp -> evd, Prop Null
@@ -489,11 +494,28 @@ let pretype_id pretype k0 loc env evdref lvar id =
(*************************************************************************)
(* Main pretyping function *)
-let interp_universe_level_name loc evd l =
- match l with
+let interp_glob_level loc evd : Misctypes.glob_level -> _ = function
| GProp -> evd, Univ.Level.prop
| GSet -> evd, Univ.Level.set
- | GType s -> interp_universe_level loc evd s
+ | GType s -> interp_level_info loc evd s
+
+let interp_instance loc evd ~len l =
+ if len != List.length l then
+ user_err ~loc ~hdr:"pretype"
+ (str "Universe instance should have length " ++ int len)
+ else
+ let evd, l' =
+ List.fold_left
+ (fun (evd, univs) l ->
+ let evd, l = interp_glob_level loc evd l in
+ (evd, l :: univs)) (evd, [])
+ l
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
+ user_err ~loc ~hdr:"pretype"
+ (str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
let pretype_global loc rigid env evd gr us =
let evd, instance =
@@ -501,21 +523,8 @@ let pretype_global loc rigid env evd gr us =
| None -> evd, None
| Some l ->
let _, ctx = Universes.unsafe_constr_of_global gr in
- let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
- let len = Array.length arr in
- if len != List.length l then
- user_err ~loc ~hdr:"pretype"
- (str "Universe instance should have length " ++ int len)
- else
- let evd, l' = List.fold_left (fun (evd, univs) l ->
- let evd, l = interp_universe_level_name loc evd l in
- (evd, l :: univs)) (evd, []) l
- in
- if List.exists (fun l -> Univ.Level.is_prop l) l' then
- user_err ~loc ~hdr:"pretype"
- (str "Universe instances cannot contain Prop, polymorphic" ++
- str " universe instances must be greater or equal to Set.");
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ let len = Univ.UContext.size ctx in
+ interp_instance loc evd ~len l
in
let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
(sigma, EConstr.of_constr c)
diff --git a/pretyping/program.ml b/pretyping/program.ml
index caa5a5c8a6..42acc5705b 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open Names
-open Term
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2703205386..52f424f751 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -239,6 +239,9 @@ sig
| Shift of int
| Update of 'a
and 'a t = 'a member list
+
+ exception IncompatibleFold2
+
val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
val empty : 'a t
val is_empty : 'a t -> bool
@@ -413,6 +416,7 @@ struct
| (_,_) -> false in
compare_rec 0 stk1 stk2
+ exception IncompatibleFold2
let fold2 f o sk1 sk2 =
let rec aux o lft1 sk1 lft2 sk2 =
let fold_array =
@@ -442,7 +446,7 @@ struct
aux o lft1 (List.rev params1) lft2 (List.rev params2)
in aux o' lft1' q1 lft2' q2
| (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
- raise (Invalid_argument "Reductionops.Stack.fold2")
+ raise IncompatibleFold2
in aux o 0 (List.rev sk1) 0 (List.rev sk2)
let rec map f x = List.map (function
@@ -1117,7 +1121,9 @@ let local_whd_state_gen flags sigma =
whrec
let raw_whd_state_gen flags env =
- let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
+ let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ())
+ ~tactic_mode:false
+ flags env sigma s) in
f
let stack_red_of_state_red f =
@@ -1127,7 +1133,7 @@ let stack_red_of_state_red f =
(* Drops the Cst_stack *)
let iterate_whd_gen refold flags env sigma s =
let rec aux t =
- let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
+ let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in
let whd_sk = Stack.map aux sk in
Stack.zip sigma ~refold (hd,whd_sk)
in aux s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 752c30a8ac..af80481569 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -81,8 +81,11 @@ module Stack : sig
val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
val compare_shape : 'a t -> 'a t -> bool
+
+ exception IncompatibleFold2
(** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
- @return the result and the lifts to apply on the terms *)
+ @return the result and the lifts to apply on the terms
+ @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
constr t -> constr t -> 'a * int * int
val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 76d0bc241f..c31212e26a 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Environ
open Evd
open EConstr
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2db0e9e881..754dacd193 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,7 +8,6 @@
(*i*)
open Names
-open Term
open EConstr
open Environ
open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9bd430e4d6..558575ccce 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,7 +8,6 @@
open Loc
open Names
-open Term
open EConstr
open Environ
open Constrexpr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c2a030bcd2..00535adb7d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -313,14 +313,13 @@ let rec execute env evdref cstr =
let j =
match EConstr.kind !evdref f with
| Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
- (* Sort-polymorphism of inductive types *)
make_judge f
(inductive_type_knowing_parameters env !evdref (ind, u) jl)
| Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
- (* Sort-polymorphism of inductive types *)
make_judge f
(constant_type_knowing_parameters env !evdref (cst, u) jl)
| _ ->
+ (* No template polymorphism *)
execute env evdref f
in
e_judge_of_apply env evdref j jl
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 532cc8baa5..661c1d8657 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1095,7 +1095,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let app = mkApp (c, Array.rev_of_list ks) in
(* let substn = unirec_rec curenvnb pb b false substn t cN in *)
unirec_rec curenvnb pb opt' substn c1 app
- with Invalid_argument "Reductionops.Stack.fold2" ->
+ with Reductionops.Stack.IncompatibleFold2 ->
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
@@ -1535,9 +1535,6 @@ let indirectly_dependent sigma c d decls =
way to see that the second hypothesis depends indirectly over 2 *)
List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
-let indirect_dependency sigma d decls =
- decls |> List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id
-
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let current_sigma = Sigma.to_evar_map current_sigma in
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:06:55 +0000