aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml15
-rw-r--r--vernac/attributes.ml2
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comArguments.ml2
-rw-r--r--vernac/comArguments.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comCoercion.ml7
-rw-r--r--vernac/comInductive.ml8
-rw-r--r--vernac/comInductive.mli8
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declareObl.ml3
-rw-r--r--vernac/g_vernac.mlg15
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml1
-rw-r--r--vernac/mltop.ml27
-rw-r--r--vernac/ppvernac.ml8
-rw-r--r--vernac/prettyp.ml14
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/vernacentries.ml54
-rw-r--r--vernac/vernacexpr.ml4
-rw-r--r--vernac/vernacinterp.ml2
24 files changed, 70 insertions, 130 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index dacef1cb18..fb61a1089f 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -240,8 +240,16 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Build the context of all arities *)
let arities_ctx =
let global_env = Global.env () in
+ let instance =
+ let open Univ in
+ Instance.of_array
+ (Array.init
+ (AUContext.size
+ (Declareops.inductive_polymorphic_context mib))
+ Level.var)
+ in
Array.fold_left (fun accu oib ->
- let pspecif = Univ.in_punivs (mib, oib) in
+ let pspecif = ((mib, oib), instance) in
let ind_type = Inductive.type_of_inductive global_env pspecif in
let indr = oib.mind_relevance in
let ind_name = Name oib.mind_typename in
@@ -356,8 +364,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
in
- if not mind.mind_typing_flags.check_template then
- let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
- ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
- else accu
+ accu
in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 68d2c3a00d..194308b77f 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -154,7 +154,6 @@ let program_mode = ref false
let () = let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "use of the program extension";
optkey = program_mode_option_name;
optread = (fun () -> !program_mode);
optwrite = (fun b -> program_mode:=b) }
@@ -188,7 +187,6 @@ let is_universe_polymorphism =
let () = let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "universe polymorphism";
optkey = universe_polymorphism_option_name;
optread = (fun () -> !b);
optwrite = ((:=) b) }
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f954915cf8..6bdb3159cf 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
in
Proofview.Goal.enter begin fun gl ->
- let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
+ let type_of_pq = Tacmach.New.pf_get_type_of gl p in
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
let u,v = destruct_ind env sigma type_of_pq
@@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
match (l1,l2) with
| (t1::q1,t2::q2) ->
Proofview.Goal.enter begin fun gl ->
- let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
if EConstr.eq_constr sigma t1 t2 then aux q1 q2
else (
+ let tt1 = Tacmach.New.pf_get_type_of gl t1 in
let u,v = try destruct_ind env sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 77bc4e4f8a..b92c9e9b71 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass =
- if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
+ if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
else tclass
in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 15077298aa..9d43debb77 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags =
let implicits = List.map (List.map snd) implicits in
let implicits_specified = match implicits with
- | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
| _ -> true in
if implicits_specified && clear_implicits_flag then
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index 71effddf67..cbc5fc15e2 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -12,6 +12,6 @@ val vernac_arguments
: section_local:bool
-> Libnames.qualid Constrexpr.or_by_notation
-> Vernacexpr.vernac_argument_status list
- -> (Names.Name.t * Impargs.implicit_kind) list list
+ -> (Names.Name.t * Glob_term.binding_kind) list list
-> Vernacexpr.arguments_modifier list
-> unit
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 625ffb5a06..d97bf6724c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -270,7 +270,7 @@ let context ~poly l =
| Some (Name id',_) -> Id.equal name id'
| _ -> false
in
- let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in
+ let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
name,b,t,impl)
ctx
in
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 56ab6f289d..2c582da495 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly =
lams
in
(* juste pour verification *)
- let _ =
- if not
- (Reductionops.is_conv_leq env sigma
- (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
+ let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in
+ let () =
+ if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f))
then
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8de1c69424..d711c9aea0 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -42,7 +42,6 @@ let should_auto_template =
let auto = ref true in
let () = declare_bool_option
{ optdepr = false;
- optname = "Automatically make some inductive types template polymorphic";
optkey = ["Auto";"Template";"Polymorphism"];
optread = (fun () -> !auto);
optwrite = (fun b -> auto := b); }
@@ -323,16 +322,15 @@ let check_named {CAst.loc;v=na} = match na with
let msg = str "Parameters must be named." in
user_err ?loc msg
-let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
+let template_polymorphism_candidate ~ctor_levels uctx params concl =
match uctx with
| Entries.Monomorphic_entry uctx ->
let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
if not concltemplate then false
- else if not template_check then true
else
let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
let params, conclunivs =
- IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
+ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
in
not (Univ.LSet.is_empty conclunivs)
| Entries.Polymorphic_entry _ -> false
@@ -385,7 +383,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
List.fold_left (fun levels c -> add_levels c levels)
param_levels ctypes
in
- template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
+ template_polymorphism_candidate ~ctor_levels uctx ctx_params concl
in
let template = match template with
| Some template ->
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index cc104b3762..1286e4a5c3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool
inductive under consideration. *)
val template_polymorphism_candidate
- : template_check:bool
- -> ctor_levels:Univ.LSet.t
+ : ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
-(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~ctor_levels uctx params
conclsort] is [true] iff an inductive with params [params],
conclusion [conclsort] and universe levels appearing in the
constructor arguments [ctor_levels] would be definable as template
polymorphic. It should have at least one universe in its
monomorphic universe context that can be made parametric in its
- conclusion sort, if one is given. If the [template_check] flag is
- false we just check that the conclusion sort is not small. *)
+ conclusion sort, if one is given. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d48e2139d1..84f8578ad4 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
- let relty = Typing.unsafe_type_of env sigma rel in
+ let relty = Retyping.get_type_of env sigma rel in
let relargty =
let error () =
user_err ?loc:(constr_loc r)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index b56b9c8ce2..dcb28b898f 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -56,7 +56,7 @@ type program_info =
let get_shrink_obligations =
Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *)
- ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"]
+ ~key:["Shrink"; "Obligations"]
~value:true
(* XXX: Is this the right place for this? *)
@@ -133,7 +133,6 @@ let add_hint local prg cst =
let get_hide_obligations =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"Hidding of Program obligations"
~key:["Hide"; "Obligations"]
~value:false
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3302231fd1..d0374bc4fa 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,7 +16,6 @@ open Util
open Names
open Glob_term
open Vernacexpr
-open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
@@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
- implicit_status = NotImplicit}] }
+ implicit_status = Explicit}] }
| "/" -> { [VolatileArg] }
| "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
@@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = NotImplicit}) items }
+ implicit_status = Explicit}) items }
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = Implicit}) items }
+ implicit_status = NonMaxImplicit}) items }
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = MaximallyImplicit}) items }
+ implicit_status = MaxImplicit}) items }
]
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
]
];
strategy_level:
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17c3e0395a..dfc4631572 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j =
str "because this term is not a type."
let explain_reference_variables sigma id c =
- (* c is intended to be a global reference *)
- let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
- pc ++ strbrk " depends on the variable " ++ Id.print id ++
+ pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++
strbrk " which is not declared in the context."
let rec pr_disjunction pr = function
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2f0b1062a7..227d2f1554 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -44,7 +44,6 @@ let elim_flag = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of induction schemes";
optkey = ["Elimination";"Schemes"];
optread = (fun () -> !elim_flag) ;
optwrite = (fun b -> elim_flag := b) }
@@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Nonrecursive";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
optwrite = (fun b -> bifinite_elim_flag := b) }
@@ -62,7 +60,6 @@ let case_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of case analysis schemes";
optkey = ["Case";"Analysis";"Schemes"];
optread = (fun () -> !case_flag) ;
optwrite = (fun b -> case_flag := b) }
@@ -71,7 +68,6 @@ let eq_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of boolean equality";
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
@@ -82,7 +78,6 @@ let eq_dec_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of decidable equality";
optkey = ["Decidable";"Equality";"Schemes"];
optread = (fun () -> !eq_dec_flag) ;
optwrite = (fun b -> eq_dec_flag := b) }
@@ -91,7 +86,6 @@ let rewriting_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname ="automatic declaration of rewriting schemes for equality types";
optkey = ["Rewriting";"Schemes"];
optread = (fun () -> !rewriting_flag) ;
optwrite = (fun b -> rewriting_flag := b) }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 865eded545..f7606f4ede 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -268,7 +268,6 @@ let warn_let_as_axiom =
let get_keep_admitted_vars =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"keep section variables in admitted proofs"
~key:["Keep"; "Admitted"; "Variables"]
~value:true
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 2bac35b08f..ab9d008659 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -11,7 +11,6 @@
open CErrors
open Util
open Pp
-open Libobject
open System
(* Code to hook Coq into the ML toplevel -- depends on having the
@@ -304,23 +303,38 @@ let _ =
(* Liboject entries of declared ML Modules *)
+(* Digest of module used to compile the file *)
+type ml_module_digest =
+ | NoDigest
+ | AnyDigest of Digest.t (* digest of any used cma / cmxa *)
+
type ml_module_object = {
mlocal : Vernacexpr.locality_flag;
- mnames : string list
+ mnames : (string * ml_module_digest) list
}
+let add_module_digest m =
+ try
+ let file = file_of_name m in
+ let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in
+ m, AnyDigest (Digest.file file)
+ with
+ | Not_found ->
+ m, NoDigest
+
let cache_ml_objects (_,{mnames=mnames}) =
- let iter obj = trigger_ml_object true true true obj in
+ let iter (obj, _) = trigger_ml_object true true true obj in
List.iter iter mnames
let load_ml_objects _ (_,{mnames=mnames}) =
- let iter obj = trigger_ml_object true false true obj in
+ let iter (obj, _) = trigger_ml_object true false true obj in
List.iter iter mnames
let classify_ml_objects ({mlocal=mlocal} as o) =
- if mlocal then Dispose else Substitute o
+ if mlocal then Libobject.Dispose else Libobject.Substitute o
-let inMLModule : ml_module_object -> obj =
+let inMLModule : ml_module_object -> Libobject.obj =
+ let open Libobject in
declare_object
{(default_object "ML-MODULE") with
cache_function = cache_ml_objects;
@@ -330,6 +344,7 @@ let inMLModule : ml_module_object -> obj =
let declare_ml_modules local l =
let l = List.map mod_of_name l in
+ let l = List.map add_module_digest l in
Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l})
let print_ml_path () =
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a1bd99c237..82132a1af6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function
let pr_br imp force x =
let left,right =
match imp with
- | Impargs.Implicit -> str "[", str "]"
- | Impargs.MaximallyImplicit -> str "{", str "}"
- | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+ | Glob_term.NonMaxImplicit -> str "[", str "]"
+ | Glob_term.MaxImplicit -> str "{", str "}"
+ | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
in
left ++ x ++ right
in
let get_arguments_like s imp tl =
- if s = None && imp = Impargs.NotImplicit then [], tl
+ if s = None && imp = Glob_term.Explicit then [], tl
else
let rec fold extra = function
| RealArg arg :: tl when
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2cd1cf7c65..32c438c724 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -211,12 +211,10 @@ let pr_template_variables = function
let print_polymorphism ref =
let poly = Global.is_polymorphic ref in
let template_poly = Global.is_template_polymorphic ref in
- let template_checked = Global.is_template_checked ref in
let template_variables = Global.get_template_polymorphic_variables ref in
[ pr_global ref ++ str " is " ++
(if poly then str "universe polymorphic"
else if template_poly then
- (if not template_checked then str "assumed " else mt()) ++
str "template universe polymorphic "
++ h 0 (pr_template_variables template_variables)
else str "not universe polymorphic") ]
@@ -260,18 +258,18 @@ let implicit_name_of_pos = function
| Constrexpr.ExplByPos (n,k) -> Anonymous
let implicit_kind_of_status = function
- | None -> Anonymous, NotImplicit
- | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
+ | None -> Anonymous, Glob_term.Explicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
let dummy = {
- Vernacexpr.implicit_status = NotImplicit;
+ Vernacexpr.implicit_status = Glob_term.Explicit;
name = Anonymous;
recarg_like = false;
notation_scope = None;
}
let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
- name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
+ name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
let rec main_implicits i renames recargs scopes impls =
if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -283,8 +281,8 @@ let rec main_implicits i renames recargs scopes impls =
let (name, implicit_status) =
match renames, impls with
| _, (Some _ as i) :: _ -> implicit_kind_of_status i
- | name::_, _ -> (name,NotImplicit)
- | [], (None::_ | []) -> (Anonymous, NotImplicit)
+ | name::_, _ -> (name,Glob_term.Explicit)
+ | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
in
let notation_scope = match scopes with
| scope :: _ -> Option.map CAst.make scope
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index cfb3248c7b..b329463cb0 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -140,7 +140,6 @@ let suggest_proof_using = ref false
let () =
Goptions.(declare_bool_option
{ optdepr = false;
- optname = "suggest Proof using";
optkey = ["Suggest";"Proof";"Using"];
optread = (fun () -> !suggest_proof_using);
optwrite = ((:=) suggest_proof_using) })
@@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"]
let () =
Goptions.(declare_stringopt_option
{ optdepr = false;
- optname = "default value for Proof using";
optkey = proof_using_opt_name;
optread = (fun () -> Option.map using_to_string !value);
optwrite = (fun b -> value := Option.map using_from_string b);
diff --git a/vernac/record.ml b/vernac/record.ml
index df9b4a0914..27bd390714 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -39,7 +39,6 @@ let primitive_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "use of primitive projections";
optkey = ["Primitive";"Projections"];
optread = (fun () -> !primitive_flag) ;
optwrite = (fun b -> primitive_flag := b) }
@@ -48,7 +47,6 @@ let typeclasses_strict = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "strict typeclass resolution";
optkey = ["Typeclasses";"Strict";"Resolution"];
optread = (fun () -> !typeclasses_strict);
optwrite = (fun b -> typeclasses_strict := b); }
@@ -57,7 +55,6 @@ let typeclasses_unique = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "unique typeclass instances";
optkey = ["Typeclasses";"Unique";"Instances"];
optread = (fun () -> !typeclasses_unique);
optwrite = (fun b -> typeclasses_unique := b); }
@@ -446,8 +443,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
univs)
param_levels fields
in
- let template_check = Environ.check_template (Global.env ()) in
- ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
+ ComInductive.template_polymorphism_candidate ~ctor_levels univs params
(Some (Sorts.sort_of_univ min_univ))
in
match template with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d011fb2e77..f8eef68997 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,27 +609,8 @@ let vernac_assumption ~atts discharge kind l nl =
| DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
-let set_template_check b =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- Global.set_typing_flags { typing_flags with Declarations.check_template = b }
-
-let is_template_check () =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- typing_flags.Declarations.check_template
-
-let () =
- let tccheck =
- { optdepr = true;
- optname = "Template universe check";
- optkey = ["Template"; "Check"];
- optread = (fun () -> is_template_check ());
- optwrite = (fun b -> set_template_check b)}
- in
- declare_bool_option tccheck
-
let is_polymorphic_inductive_cumulativity =
declare_bool_option_and_ref ~depr:false ~value:false
- ~name:"Polymorphic inductive cumulativity"
~key:["Polymorphic"; "Inductive"; "Cumulativity"]
let should_treat_as_cumulative cum poly =
@@ -645,7 +626,6 @@ let should_treat_as_cumulative cum poly =
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"Uniform inductive parameters"
~key:["Uniform"; "Inductive"; "Parameters"]
~value:false
@@ -1238,7 +1218,6 @@ let vernac_generalizable ~local =
let () =
declare_bool_option
{ optdepr = false;
- optname = "allow sprop";
optkey = ["Allow";"StrictProp"];
optread = (fun () -> Global.sprop_allowed());
optwrite = Global.set_allow_sprop }
@@ -1246,7 +1225,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "silent";
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
optwrite = ((:=) Flags.quiet) }
@@ -1254,7 +1232,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments";
optkey = ["Implicit";"Arguments"];
optread = Impargs.is_implicit_args;
optwrite = Impargs.make_implicit_args }
@@ -1262,7 +1239,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "strict implicit arguments";
optkey = ["Strict";"Implicit"];
optread = Impargs.is_strict_implicit_args;
optwrite = Impargs.make_strict_implicit_args }
@@ -1270,7 +1246,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "strong strict implicit arguments";
optkey = ["Strongly";"Strict";"Implicit"];
optread = Impargs.is_strongly_strict_implicit_args;
optwrite = Impargs.make_strongly_strict_implicit_args }
@@ -1278,7 +1253,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "contextual implicit arguments";
optkey = ["Contextual";"Implicit"];
optread = Impargs.is_contextual_implicit_args;
optwrite = Impargs.make_contextual_implicit_args }
@@ -1286,7 +1260,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit status of reversible patterns";
optkey = ["Reversible";"Pattern";"Implicit"];
optread = Impargs.is_reversible_pattern_implicit_args;
optwrite = Impargs.make_reversible_pattern_implicit_args }
@@ -1294,7 +1267,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "maximal insertion of implicit";
optkey = ["Maximal";"Implicit";"Insertion"];
optread = Impargs.is_maximal_implicit_args;
optwrite = Impargs.make_maximal_implicit_args }
@@ -1302,7 +1274,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "coercion printing";
optkey = ["Printing";"Coercions"];
optread = (fun () -> !Constrextern.print_coercions);
optwrite = (fun b -> Constrextern.print_coercions := b) }
@@ -1310,7 +1281,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "printing of existential variable instances";
optkey = ["Printing";"Existential";"Instances"];
optread = (fun () -> !Detyping.print_evar_arguments);
optwrite = (:=) Detyping.print_evar_arguments }
@@ -1318,7 +1288,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments printing";
optkey = ["Printing";"Implicit"];
optread = (fun () -> !Constrextern.print_implicits);
optwrite = (fun b -> Constrextern.print_implicits := b) }
@@ -1326,7 +1295,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments defensive printing";
optkey = ["Printing";"Implicit";"Defensive"];
optread = (fun () -> !Constrextern.print_implicits_defensive);
optwrite = (fun b -> Constrextern.print_implicits_defensive := b) }
@@ -1334,7 +1302,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "projection printing using dot notation";
optkey = ["Printing";"Projections"];
optread = (fun () -> !Constrextern.print_projections);
optwrite = (fun b -> Constrextern.print_projections := b) }
@@ -1342,7 +1309,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "notations printing";
optkey = ["Printing";"Notations"];
optread = (fun () -> not !Constrextern.print_no_symbol);
optwrite = (fun b -> Constrextern.print_no_symbol := not b) }
@@ -1350,7 +1316,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "raw printing";
optkey = ["Printing";"All"];
optread = (fun () -> !Flags.raw_print);
optwrite = (fun b -> Flags.raw_print := b) }
@@ -1358,7 +1323,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the level of inlining during functor application";
optkey = ["Inline";"Level"];
optread = (fun () -> Some (Flags.get_inline_level ()));
optwrite = (fun o ->
@@ -1368,7 +1332,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
optwrite = Global.set_share_reduction }
@@ -1376,7 +1339,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "display compact goal contexts";
optkey = ["Printing";"Compact";"Contexts"];
optread = (fun () -> Printer.get_compact_context());
optwrite = (fun b -> Printer.set_compact_context b) }
@@ -1384,7 +1346,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the printing depth";
optkey = ["Printing";"Depth"];
optread = Topfmt.get_depth_boxes;
optwrite = Topfmt.set_depth_boxes }
@@ -1392,7 +1353,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the printing width";
optkey = ["Printing";"Width"];
optread = Topfmt.get_margin;
optwrite = Topfmt.set_margin }
@@ -1400,7 +1360,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "printing of universes";
optkey = ["Printing";"Universes"];
optread = (fun () -> !Constrextern.print_universes);
optwrite = (fun b -> Constrextern.print_universes:=b) }
@@ -1408,7 +1367,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "dumping bytecode after compilation";
optkey = ["Dump";"Bytecode"];
optread = (fun () -> !Cbytegen.dump_bytecode);
optwrite = (:=) Cbytegen.dump_bytecode }
@@ -1416,7 +1374,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "dumping VM lambda code after compilation";
optkey = ["Dump";"Lambda"];
optread = (fun () -> !Clambda.dump_lambda);
optwrite = (:=) Clambda.dump_lambda }
@@ -1424,7 +1381,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "explicitly parsing implicit arguments";
optkey = ["Parsing";"Explicit"];
optread = (fun () -> !Constrintern.parsing_explicit);
optwrite = (fun b -> Constrintern.parsing_explicit := b) }
@@ -1432,7 +1388,6 @@ let () =
let () =
declare_string_option ~preprocess:CWarnings.normalize_flags_string
{ optdepr = false;
- optname = "warnings display";
optkey = ["Warnings"];
optread = CWarnings.get_flags;
optwrite = CWarnings.set_flags }
@@ -1440,7 +1395,6 @@ let () =
let () =
declare_string_option
{ optdepr = false;
- optname = "native_compute profiler output";
optkey = ["NativeCompute"; "Profile"; "Filename"];
optread = Nativenorm.get_profile_filename;
optwrite = Nativenorm.set_profile_filename }
@@ -1448,7 +1402,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "enable native compute profiling";
optkey = ["NativeCompute"; "Profiling"];
optread = Nativenorm.get_profiling_enabled;
optwrite = Nativenorm.set_profiling_enabled }
@@ -1456,7 +1409,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "enable native compute timing";
optkey = ["NativeCompute"; "Timing"];
optread = Nativenorm.get_timing_enabled;
optwrite = Nativenorm.set_timing_enabled }
@@ -1464,7 +1416,6 @@ let () =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "guard checking";
optkey = ["Guard"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
optwrite = (fun b -> Global.set_check_guarded b) }
@@ -1472,7 +1423,6 @@ let _ =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "positivity/productivity checking";
optkey = ["Positivity"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
optwrite = (fun b -> Global.set_check_positive b) }
@@ -1480,7 +1430,6 @@ let _ =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "universes checking";
optkey = ["Universe"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
optwrite = (fun b -> Global.set_check_universes b) }
@@ -1589,7 +1538,7 @@ let query_command_selector ?loc = function
let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
let glopt = query_command_selector glopt in
let sigma, env = get_current_context_of_args ~pstate glopt in
- let sigma, c = interp_open_constr env sigma rc in
+ let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
Evarconv.check_problems_are_solved env sigma;
let sigma = Evd.minimize_universes sigma in
@@ -1795,7 +1744,6 @@ let search_output_name_only = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "output-name-only search";
optkey = ["Search";"Output";"Name";"Only"];
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 1daa244986..22a8de7f99 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -254,7 +254,7 @@ type vernac_one_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : Impargs.implicit_kind;
+ implicit_status : Glob_term.binding_kind;
}
type vernac_argument_status =
@@ -386,7 +386,7 @@ type nonrec vernac_expr =
| VernacArguments of
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
+ (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) *
arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c14fc78462..1ec09b6beb 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"]
let () =
Goptions.declare_string_option Goptions.{
optdepr = false;
- optname = "default proof mode" ;
optkey = proof_mode_opt_name;
optread = get_default_proof_mode_opt;
optwrite = set_default_proof_mode_opt;
@@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
let () = let open Goptions in
declare_int_option
{ optdepr = false;
- optname = "the default timeout";
optkey = ["Default";"Timeout"];
optread = (fun () -> !default_timeout);
optwrite = ((:=) default_timeout) }
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:16:05 +0000