aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml5
-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/comInductive.ml7
-rw-r--r--vernac/comInductive.mli8
-rw-r--r--vernac/g_vernac.mlg15
-rw-r--r--vernac/ppvernac.ml8
-rw-r--r--vernac/prettyp.ml14
-rw-r--r--vernac/record.ml3
-rw-r--r--vernac/vernacentries.ml20
-rw-r--r--vernac/vernacexpr.ml4
13 files changed, 32 insertions, 60 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index dacef1cb18..9f92eba729 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -356,8 +356,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/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/comInductive.ml b/vernac/comInductive.ml
index 8de1c69424..dce0a70f72 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -323,16 +323,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 +384,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/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/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/record.ml b/vernac/record.ml
index df9b4a0914..f6945838d7 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -446,8 +446,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..fd588f5b15 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,24 +609,6 @@ 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"
@@ -1589,7 +1571,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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:27:11 +0000