aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml13
-rw-r--r--pretyping/cbv.ml1
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/program.ml3
-rw-r--r--pretyping/reductionops.ml6
-rw-r--r--pretyping/reductionops.mli12
-rw-r--r--pretyping/retyping.ml16
-rw-r--r--pretyping/typeclasses.ml1
-rw-r--r--pretyping/typing.ml9
-rw-r--r--pretyping/unification.ml3
-rw-r--r--pretyping/vnorm.ml2
15 files changed, 36 insertions, 45 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 36f35a67c3..59ca418a39 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Globnames
-open Term
open Constr
open Context
open Environ
@@ -78,14 +77,14 @@ let rename_type ty ref =
let rec rename_type_aux c = function
| [] -> c
| rename :: rest as renamings ->
- match kind_of_type c with
- | ProdType (old, s, t) ->
+ match Constr.kind c with
+ | Prod (old, s, t) ->
mkProd (name_override old rename, s, rename_type_aux t rest)
- | LetInType(old, s, b, t) ->
+ | LetIn (old, s, b, t) ->
mkLetIn (old ,s, b, rename_type_aux t renamings)
- | CastType (t,_) -> rename_type_aux t renamings
- | SortType _ -> c
- | AtomicType _ -> c in
+ | Cast (t,_, _) -> rename_type_aux t renamings
+ | _ -> c
+ in
try rename_type_aux ty (arguments_names ref)
with Not_found -> ty
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2b7ccbbcad..11c97221ec 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk =
let get_debug_cbv = Goptions.declare_bool_option_and_ref
~depr:false
~value:false
- ~name:"cbv visited constants display"
~key:["Debug";"Cbv"]
(* Reduction of primitives *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c7f9a8f00..c4aa3479bf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -36,7 +36,6 @@ open Globnames
let get_use_typeclasses_for_conversion =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"use typeclass resolution during conversion"
~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
~value:true
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b042437a22..83078660c5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value
let () = declare_bool_option
{ optdepr = false;
- optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
optread = force_wildcard;
optwrite = (:=) wildcard_value }
@@ -237,7 +236,6 @@ let fast_name_generation = ref false
let () = declare_bool_option {
optdepr = false;
- optname = "fast bound name generation algorithm";
optkey = ["Fast";"Name";"Printing"];
optread = (fun () -> !fast_name_generation);
optwrite = (:=) fast_name_generation;
@@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
optread = synthetize_type;
optwrite = (:=) synth_type_value }
@@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
optread = reverse_matching;
optwrite = (:=) reverse_matching_value }
@@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value
let () = declare_bool_option
{ optdepr = false;
- optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
@@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "factorization of \"match\" patterns in printing";
optkey = ["Printing";"Factorizable";"Match";"Patterns"];
optread = (fun () -> !print_factorize_match_patterns);
optwrite = (fun b -> print_factorize_match_patterns := b) }
@@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "possible use of \"match\" default pattern in printing";
optkey = ["Printing";"Allow";"Match";"Default";"Clause"];
optread = (fun () -> !print_allow_match_default_clause);
optwrite = (fun b -> print_allow_match_default_clause := b) }
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c21af82659..c67019c7ac 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -50,8 +50,6 @@ let default_flags env =
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to Evarconv unification";
optkey = ["Debug";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
@@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option {
let debug_ho_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print higher-order unification debug information";
optkey = ["Debug";"HO";"Unification"];
optread = (fun () -> !debug_ho_unification);
optwrite = (fun a -> debug_ho_unification:=a);
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 816a8c4703..a4406aeba1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -29,7 +29,7 @@ open Context.Rel.Declaration
let type_of_inductive env (ind,u) =
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
- Inductive.type_of_inductive env (specif,u)
+ Inductive.type_of_inductive (specif,u)
(* Return type as quoted by the user *)
let type_of_constructor env (cstr,u) =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2d98d48aa0..ac1a4e88ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix =
let is_strict_universe_declarations =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"strict universe declaration"
~key:["Strict";"Universe";"Declaration"]
~value:true
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..9c478844aa 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -78,7 +78,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "preferred transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
@@ -86,7 +85,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program cases";
optkey = ["Program";"Cases"];
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
@@ -94,7 +92,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program generalized coercion";
optkey = ["Program";"Generalized";"Coercion"];
optread = (fun () -> !program_generalized_coercion);
optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d5beebe690..838bf22c66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -32,8 +32,6 @@ exception Elimconst
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Generate weak constraints between Irrelevant universes";
optkey = ["Cumulativity";"Weak";"Constraints"];
optread = (fun () -> not !UState.drop_weak_constraints);
optwrite = (fun a -> UState.drop_weak_constraints:=not a);
@@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries)
let debug_RAKAM = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states of the Reductionops abstract machine";
optkey = ["Debug";"RAKAM"];
optread = (fun () -> !debug_RAKAM);
optwrite = (fun a -> debug_RAKAM:=a);
@@ -1711,7 +1707,7 @@ let splay_arity env sigma c =
let l, c = splay_prod env sigma c in
match EConstr.kind sigma c with
| Sort s -> l,s
- | _ -> invalid_arg "splay_arity"
+ | _ -> raise Reduction.NotArity
let sort_of_arity env sigma c = snd (splay_arity env sigma c)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e72f5f2793..c539ec55ed 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr
val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
+val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr
+
val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t
+(** Raises [Reduction.NotArity] *)
+
val sort_of_arity : env -> evar_map -> constr -> ESorts.t
+(** Raises [Reduction.NotArity] *)
+
val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
-val splay_prod_assum :
- env -> evar_map -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
type 'a miota_args = {
mP : constr; (** the result type *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d2af957b54..87fe4cfcda 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma =
| _ -> decomp_sort env sigma (type_of env t)
and type_of_global_reference_knowing_parameters env c args =
- let argtyps =
- Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
match EConstr.kind sigma c with
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
let mip = lookup_mind_specif env ind in
- EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
- ~polyprop env (mip, u) argtyps
- with Reduction.NotArity -> retype_error NotAnArity)
+ let paramtyps = Array.map_to_list (fun arg () ->
+ let t = type_of env arg in
+ let s = try Reductionops.sort_of_arity env sigma t
+ with Reduction.NotArity -> retype_error NotAnArity
+ in
+ Sorts.univ_of_sort (ESorts.kind sigma s))
+ args
+ in
+ EConstr.of_constr
+ (Inductive.type_of_inductive_knowing_parameters
+ ~polyprop (mip, u) paramtyps)
| Construct (cstr, u) ->
let u = EInstance.kind sigma u in
EConstr.of_constr (type_of_constructor env (cstr, u))
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d5c8c3bd19..aa2e96c2d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
let get_typeclasses_unique_solutions =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"check that typeclasses proof search returns unique solutions"
~key:["Typeclasses";"Unique";"Solutions"]
~value:false
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b4c19775a7..f067c075bf 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -38,8 +38,11 @@ let meta_type evd mv =
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
- let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
- Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+ let paramstyp = Array.map_to_list (fun j () ->
+ let s = Reductionops.sort_of_arity env sigma j.uj_type in
+ Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl
+ in
+ Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
let type_judgment env sigma j =
match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) =
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
let u = EInstance.kind sigma u in
- let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+ let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in
let sigma = Evd.add_constraints sigma csts in
sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2157c4ef6a..5b87603d54 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname = "Unification is keyed";
optkey = ["Keyed";"Unification"];
optread = (fun () -> !keyed_unification);
optwrite = (fun a -> keyed_unification:=a);
@@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to tactic unification";
optkey = ["Debug";"Tactic";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 885fc8980d..b04e59734d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
let type_of_ind env (ind, u) =
- type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
+ type_of_inductive (Inductive.lookup_mind_specif env ind, u)
let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
let rtbl = mip.mind_reloc_tbl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:43:47 +0000