aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.mli1
-rw-r--r--pretyping/classops.ml1
-rw-r--r--pretyping/classops.mli1
-rw-r--r--pretyping/coercion.ml5
-rw-r--r--pretyping/coercion.mli1
-rw-r--r--pretyping/constr_matching.ml1
-rw-r--r--pretyping/detyping.ml3
-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/glob_ops.ml9
-rw-r--r--pretyping/inductiveops.ml1
-rw-r--r--pretyping/patternops.ml12
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--pretyping/pretype_errors.ml1
-rw-r--r--pretyping/pretyping.ml7
-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
26 files changed, 28 insertions, 50 deletions
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 e9b3d197bc..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 *)
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 d553506228..2334be9664 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -87,7 +87,6 @@ let rec build_lambda sigma vars ctx m = match vars with
| n :: vars ->
(* change [ x1 ... xn y z1 ... zm |- t ] into
[ x1 ... xn z1 ... zm |- lam y. t ] *)
- let len = List.length ctx in
let pre, suf = List.chop (pred n) ctx in
let (na, t, suf) = match suf with
| [] -> assert false
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba4086795..1eec85f455 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
@@ -696,7 +695,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/glob_ops.ml b/pretyping/glob_ops.ml
index 7fb539fb5b..ebbfa195f0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,7 +12,6 @@ open Nameops
open Globnames
open Misctypes
open Glob_term
-open Evar_kinds
(* Untyped intermediate terms, after ASTs and before constr. *)
@@ -62,18 +61,14 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
| CastNative t1, CastNative t2 -> eq t1 t2
| _ -> false
-let matching_var_kind_eq k1 k2 = match k1, k2 with
-| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
-| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
-| _ -> false
-
let rec glob_constr_eq c1 c2 = match c1, c2 with
| GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2
| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
| GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
Id.equal id1 id2 &&
List.equal instance_eq arg1 arg2
-| GPatVar (_, k1), GPatVar (_, k2) -> matching_var_kind_eq k1 k2
+| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+ (b1 : bool) == b2 && Id.equal pat1 pat2
| GApp (_, f1, arg1), GApp (_, f2, arg2) ->
glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) ->
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/patternops.ml b/pretyping/patternops.ml
index b310da9a37..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 =
@@ -145,7 +144,7 @@ let pattern_of_constr env sigma t =
match kind_of_term f with
| Evar (evk,args) ->
(match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
+ Evar_kinds.MatchingVar (true,id) -> Some id
| _ -> None)
| _ -> None
with
@@ -158,11 +157,10 @@ let pattern_of_constr env sigma t =
pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
| Evar (evk,ctxt) ->
(match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
- PMeta (Some id)
+ | Evar_kinds.MatchingVar (b,id) ->
+ assert (not b); PMeta (Some id)
| Evar_kinds.GoalEvar ->
PEvar (evk,Array.map (pattern_of_constr env) ctxt)
- | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
| Case (ci,p,a,br) ->
@@ -329,12 +327,12 @@ let rec pat_of_raw metas vars = function
| GVar (_,id) ->
(try PRel (List.index Name.equal (Name id) vars)
with Not_found -> PVar id)
- | GPatVar (_,Evar_kinds.FirstOrderPatVar n) ->
+ | GPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
| GRef (_,gr,_) ->
PRef (canonical_gr gr)
(* Hack to avoid rewriting a complete interpretation of patterns *)
- | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) ->
+ | GApp (_, GPatVar (_,(true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
| GApp (_,c,cl) ->
PApp (pat_of_raw metas vars c,
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 6c490045ca..68ef976592 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
@@ -195,7 +194,7 @@ let _ =
(** Miscellaneous interpretation functions *)
let interp_universe_level_name evd (loc,s) =
let names, _ = Global.global_universe_names () in
- if CString.string_contains s "." then
+ if CString.string_contains ~where:s ~what:"." then
match List.rev (CString.split '.' s) with
| [] -> anomaly (str"Invalid universe name " ++ str s)
| n :: dp ->
@@ -596,13 +595,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | GPatVar (loc,kind) ->
+ | GPatVar (loc,(someta,n)) ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
| None -> new_type_evar env evdref loc in
- let k = Evar_kinds.MatchingVar kind in
+ let k = Evar_kinds.MatchingVar (someta,n) in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (loc, k, naming, None) ->
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-05-02 17:31:36 +0000