aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml36
-rw-r--r--vernac/assumptions.mli5
-rw-r--r--vernac/comInductive.ml74
-rw-r--r--vernac/comInductive.mli6
-rw-r--r--vernac/g_vernac.mlg8
-rw-r--r--vernac/metasyntax.ml76
-rw-r--r--vernac/metasyntax.mli9
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/record.ml28
-rw-r--r--vernac/record.mli3
-rw-r--r--vernac/vernacentries.ml52
-rw-r--r--vernac/vernacexpr.ml1
-rw-r--r--vernac/vernacinterp.ml5
-rw-r--r--vernac/vernacinterp.mli4
15 files changed, 208 insertions, 109 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 765f962e99..0bcd3c64eb 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function
let rec lookup_module_in_impl mp =
match mp with
- | MPfile _ -> raise Not_found
+ | MPfile _ -> Global.lookup_module mp
| MPbound _ -> assert false
| MPdot (mp',lab') ->
if ModPath.equal mp' (Global.current_modpath ()) then
@@ -213,25 +213,25 @@ let rec traverse current ctx accu t = match Constr.kind t with
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
let data, ax2ty =
- let already_in = Refmap_env.mem obj data in
+ let already_in = GlobRef.Map_env.mem obj data in
match body () with
| None ->
let data =
- if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+ if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
let ax2ty =
if Option.is_empty inhabits then ax2ty else
let ty = Option.get inhabits in
- try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty
- with Not_found -> Refmap_env.add obj [ty] ax2ty in
+ try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty
+ with Not_found -> GlobRef.Map_env.add obj [ty] ax2ty in
data, ax2ty
| Some body ->
if already_in then data, ax2ty else
let contents,data,ax2ty =
traverse (label_of obj) Context.Rel.empty
- (Refset_env.empty,data,ax2ty) body in
- Refmap_env.add obj contents data, ax2ty
+ (GlobRef.Set_env.empty,data,ax2ty) body in
+ GlobRef.Map_env.add obj contents data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects the references occurring in the declaration of mutual inductive
definitions. All the constructors and names of a mutual inductive
@@ -244,14 +244,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
where I_0, I_1, ... are in the same mutual definition and c_ij
are all their constructors. *)
- if Refmap_env.mem firstind_ref data then data, ax2ty else
+ if GlobRef.Map_env.mem firstind_ref data then data, ax2ty else
let mib = lookup_mind mind in
(* Collects references of parameters *)
let param_ctx = mib.mind_params_ctxt in
let nparam = List.length param_ctx in
let accu =
traverse_context label Context.Rel.empty
- (Refset_env.empty, data, ax2ty) param_ctx
+ (GlobRef.Set_env.empty, data, ax2ty) param_ctx
in
(* Build the context of all arities *)
let arities_ctx =
@@ -283,14 +283,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Maps all these dependencies to inductives and constructors*)
let data = Array.fold_left_i (fun n data oib ->
let ind = (mind, n) in
- let data = Refmap_env.add (IndRef ind) contents data in
+ let data = GlobRef.Map_env.add (IndRef ind) contents data in
Array.fold_left_i (fun k data _ ->
- Refmap_env.add (ConstructRef (ind, k+1)) contents data
+ GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
) data oib.mind_consnames) data mib.mind_packets
in
data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects references in a rel_context. *)
and traverse_context current ctx accu ctxt =
@@ -307,7 +307,7 @@ and traverse_context current ctx accu ctxt =
let traverse current t =
let () = modcache := MPmap.empty in
- traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+ traverse current Context.Rel.empty (GlobRef.Set_env.empty, GlobRef.Map_env.empty, GlobRef.Map_env.empty) t
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
@@ -330,12 +330,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let accu =
if cb.const_typing_flags.check_guarded then accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
in
if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
let t = type_of_constant cb in
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Constant kn,l)) t accu
else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
let t = type_of_constant cb in
@@ -350,7 +350,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
if mind.mind_typing_flags.check_guarded then
accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
in
- Refmap_env.fold fold graph ContextObjectMap.empty
+ GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 751e79d89c..aead345d8c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -10,7 +10,6 @@
open Names
open Constr
-open Globnames
open Printer
(** Collects all the objects on which a term directly relies, bypassing kernel
@@ -22,8 +21,8 @@ open Printer
*)
val traverse :
Label.t -> constr ->
- (Refset_env.t * Refset_env.t Refmap_env.t *
- (Label.t * Constr.rel_context * types) list Refmap_env.t)
+ (GlobRef.Set_env.t * GlobRef.Set_env.t GlobRef.Map_env.t *
+ (Label.t * Constr.rel_context * types) list GlobRef.Map_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 716c40dbff..fb9d21c429 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -35,6 +35,18 @@ module RelDecl = Context.Rel.Declaration
(* 3b| Mutual inductive definitions *)
+let should_auto_template =
+ let open Goptions in
+ 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); }
+ in
+ fun () -> !auto
+
let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
| CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
@@ -113,17 +125,16 @@ let rec check_anonymous_type ind =
| GCast (e, _) -> check_anonymous_type e
| _ -> false
-let make_conclusion_flexible sigma ty poly =
- if poly && Term.isArity ty then
- let _, concl = Term.destArity ty in
- match concl with
- | Type u ->
- (match Univ.universe_level u with
+let make_conclusion_flexible sigma = function
+ | None -> sigma
+ | Some s ->
+ (match EConstr.ESorts.kind sigma s with
+ | Type u ->
+ (match Univ.universe_level u with
| Some u ->
Evd.make_flexible_variable sigma ~algebraic:true u
| None -> sigma)
- | _ -> sigma
- else sigma
+ | _ -> sigma)
let is_impredicative env u =
u = Prop || (is_impredicative_set env && u = Set)
@@ -133,10 +144,12 @@ let interp_ind_arity env sigma ind =
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reductionops.is_arity env sigma t) then
+ match Reductionops.sort_of_arity env sigma t with
+ | exception Invalid_argument _ ->
user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
- in
- sigma, (t, pseudo_poly, impls)
+ | s ->
+ let concl = if pseudo_poly then Some s else None in
+ sigma, (t, concl, impls)
let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
@@ -335,7 +348,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
List.iter check_param paramsl;
if not (List.is_empty uparamsl) && not (List.is_empty notations)
@@ -363,7 +376,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, _, impls) -> userimpls @
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
- let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
+ let arities = List.map pi1 arities and arityconcl = List.map pi2 arities in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -402,13 +415,14 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
let nf = Evarutil.nf_evars_universes sigma in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
- let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+ let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map nf arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
+ let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
let uctx = Evd.check_univ_decl ~poly sigma decl in
List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
@@ -418,13 +432,23 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
- mind_entry_typename = ind.ind_name;
- mind_entry_arity = arity;
- mind_entry_template = template;
- mind_entry_consnames = cnames;
- mind_entry_lc = ctypes
- }) indl arities aritypoly constructors in
+ let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+ let template = match template with
+ | Some template ->
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None ->
+ should_auto_template () && not poly &&
+ Option.cata (fun s -> not (Sorts.is_small s)) false concl
+ in
+ { mind_entry_typename = ind.ind_name;
+ mind_entry_arity = arity;
+ mind_entry_template = template;
+ mind_entry_consnames = cnames;
+ mind_entry_lc = ctypes
+ })
+ indl arities arityconcl constructors
+ in
let impls =
let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
@@ -454,8 +478,8 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
InferCumulativity.infer_inductive env_ar mind_ent
else mind_ent), Evd.universe_binders sigma, impls
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
- interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite =
+ interp_mutual_inductive_gen (Global.env()) ~template ([],paramsl,indl) notations cum poly prv finite
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -543,11 +567,11 @@ type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
-let do_mutual_inductive indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template indl cum poly prv ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
- let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
+ let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template indl ntns cum poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 4e30ed7de5..8a2c9b8719 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,7 +24,7 @@ type uniform_inductive_flag =
| NonUniformParameters
val do_mutual_inductive :
- (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+ template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
Declarations.recursivity_kind -> unit
@@ -45,6 +45,8 @@ val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
+val should_auto_template : unit -> bool
+
(** Exported for Funind *)
(** Extracting the semantical components out of the raw syntax of mutual
@@ -67,6 +69,6 @@ val extract_mutual_inductive_declaration_components :
(** Typing mutual inductive definitions *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+ template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> Declarations.recursivity_kind ->
mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74516e320c..44c0159d1b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram
info = hint_info ->
{ VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+ (* Should be in syntax, but camlp5 would not factorize *)
+ | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
+ { VernacDeclareScope sc }
+
(* System directory *)
| IDENT "Pwd" -> { VernacChdir None }
| IDENT "Cd" -> { VernacChdir None }
@@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
-> { VernacSyntaxExtension (false, (s,l)) }
- (* "Print" "Grammar" should be here but is in "command" entry in order
- to factorize with other "Print"-based vernac entries *)
+ (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
+ to factorize with other "Print"-based or "Declare"-based vernac entries *)
] ]
;
only_parsing:
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d66a121437..2e5e11bb09 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1306,8 +1306,18 @@ type notation_obj = {
notobj_notation : notation * notation_location;
}
-let load_notation _ (_, nobj) =
- Option.iter Notation.declare_scope nobj.notobj_scope
+let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
+ (* When the default shall be to require that a scope already exists *)
+ (* the call to ensure_scope will have to be removed *)
+ if silently_define_scope_if_undefined then
+ (* Don't warn if the scope is not defined: *)
+ (* there was already a warning at "cache" time *)
+ Option.iter Notation.declare_scope nobj.notobj_scope
+ else
+ Option.iter Notation.ensure_scope nobj.notobj_scope
+
+let load_notation =
+ load_notation_common true
let open_notation i (_, nobj) =
let scope = nobj.notobj_scope in
@@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) =
end
let cache_notation o =
- load_notation 1 o;
+ load_notation_common false 1 o;
open_notation 1 o
let subst_notation (subst, nobj) =
@@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
add_notation local env c (df,modifiers) sc
(**********************************************************************)
-(* Delimiters and classes bound to scopes *)
+(* Scopes, delimiters and classes bound to scopes *)
type scope_command =
- | ScopeDelim of string
+ | ScopeDeclare
+ | ScopeDelimAdd of string
+ | ScopeDelimRemove
| ScopeClasses of scope_class list
- | ScopeRemove
-
-let load_scope_command _ (_,(scope,dlm)) =
- Notation.declare_scope scope
-let open_scope_command i (_,(scope,o)) =
+let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) =
+ let declare_scope_if_needed =
+ if silently_define_scope_if_undefined then Notation.declare_scope
+ else Notation.ensure_scope in
+ match o with
+ | ScopeDeclare -> Notation.declare_scope scope
+ (* When the default shall be to require that a scope already exists *)
+ (* the call to declare_scope_if_needed will have to be removed below *)
+ | ScopeDelimAdd dlm -> declare_scope_if_needed scope
+ | ScopeDelimRemove -> declare_scope_if_needed scope
+ | ScopeClasses cl -> declare_scope_if_needed scope
+
+let load_scope_command =
+ load_scope_command_common true
+
+let open_scope_command i (_,(local,scope,o)) =
if Int.equal i 1 then
match o with
- | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+ | ScopeDeclare -> ()
+ | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm
+ | ScopeDelimRemove -> Notation.remove_delimiters scope
| ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
- | ScopeRemove -> Notation.remove_delimiters scope
let cache_scope_command o =
- load_scope_command 1 o;
+ load_scope_command_common false 1 o;
open_scope_command 1 o
-let subst_scope_command (subst,(scope,o as x)) = match o with
+let subst_scope_command (subst,(local,scope,o as x)) = match o with
| ScopeClasses cl ->
let cl' = List.map_filter (subst_scope_class subst) cl in
let cl' =
if List.for_all2eq (==) cl cl' then cl
else cl' in
- scope, ScopeClasses cl'
+ local, scope, ScopeClasses cl'
| _ -> x
-let inScopeCommand : scope_name * scope_command -> obj =
+let classify_scope_command (local, _, _ as o) =
+ if local then Dispose else Substitute o
+
+let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
declare_object {(default_object "DELIMITERS") with
cache_function = cache_scope_command;
open_function = open_scope_command;
load_function = load_scope_command;
subst_function = subst_scope_command;
- classify_function = (fun obj -> Substitute obj)}
+ classify_function = classify_scope_command}
+
+let declare_scope local scope =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare))
-let add_delimiters scope key =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
+let add_delimiters local scope key =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key))
-let remove_delimiters scope =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+let remove_delimiters local scope =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove))
-let add_class_scope scope cl =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
+let add_class_scope local scope cl =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
(* Check if abbreviation to a name and avoid early insertion of
maximal implicit arguments *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 73bee7121b..38dbdf7e41 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr ->
val add_notation_extra_printing_rule : string -> string -> string -> unit
-(** Declaring delimiter keys and default scopes *)
+(** Declaring scopes, delimiter keys and default scopes *)
-val add_delimiters : scope_name -> string -> unit
-val remove_delimiters : scope_name -> unit
-val add_class_scope : scope_name -> scope_class list -> unit
+val declare_scope : locality_flag -> scope_name -> unit
+val add_delimiters : locality_flag -> scope_name -> string -> unit
+val remove_delimiters : locality_flag -> scope_name -> unit
+val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
(** Add only the interpretation of a notation that already has pa/pp rules *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 14d7642328..3987e53bc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -523,11 +523,11 @@ let declare_mutual_definition l =
(List.map (fun x ->
let subs, typ = (subst_body true x) in
let env = Global.env () in
- let sigma = Evd.from_env env in
+ let sigma = Evd.from_ctx x.prg_ctx in
let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
- let term = EConstr.Unsafe.to_constr term in
- let typ = EConstr.Unsafe.to_constr typ in
+ let term = EConstr.to_constr sigma term in
+ let typ = EConstr.to_constr sigma typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 93e4e89a12..63e9e4fe49 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -635,6 +635,10 @@ open Pputils
keyword (if opening then "Open " else "Close ") ++
keyword "Scope" ++ spc() ++ str sc
)
+ | VernacDeclareScope sc ->
+ return (
+ keyword "Declare Scope" ++ spc () ++ str sc
+ )
| VernacDelimiters (sc,Some key) ->
return (
keyword "Delimit Scope" ++ spc () ++ str sc ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b5c538df2..d36586d062 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -393,14 +393,14 @@ open Typeclasses
let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
let nparams = List.length params in
- let template, ctx =
+ let poly, ctx =
match univs with
| Monomorphic_ind_entry ctx ->
- template, Monomorphic_const_entry Univ.ContextSet.empty
+ false, Monomorphic_const_entry Univ.ContextSet.empty
| Polymorphic_ind_entry ctx ->
- false, Polymorphic_const_entry ctx
+ true, Polymorphic_const_entry ctx
| Cumulative_ind_entry cumi ->
- false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+ true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -417,6 +417,18 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
+ let template =
+ match template with
+ | Some template, _ ->
+ (* templateness explicitly requested *)
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None, template ->
+ (* auto detect template *)
+ ComInductive.should_auto_template () && template && not poly &&
+ let _, s = Reduction.dest_arity (Global.env()) arity in
+ not (Sorts.is_small s)
+ in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_template = template;
@@ -441,7 +453,6 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
let build = ConstructRef cstr in
- let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
rsp
@@ -656,13 +667,14 @@ let extract_record_data records =
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure kind cum poly finite records =
+let definition_structure kind ~template cum poly finite records =
let () = check_unique_names records in
let () = check_priorities kind records in
let pl, ps, data = extract_record_data records in
- let pl, univs, template, params, implpars, data =
+ let pl, univs, auto_template, params, implpars, data =
States.with_state_protection (fun () ->
- typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+ typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+ let template = template, auto_template in
match kind with
| Class def ->
let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
diff --git a/vernac/record.mli b/vernac/record.mli
index 567f2b3138..055a17895a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,8 @@ val declare_projections :
(Name.t * bool) list * Constant.t option list
val definition_structure :
- inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+ inductive_kind -> template:bool option ->
+ Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
Declarations.recursivity_kind ->
(coercion_flag *
Names.lident *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f7ba305374..e6b3721134 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -403,17 +403,24 @@ let dump_global r =
(**********)
(* Syntax *)
-let vernac_syntax_extension atts infix l =
+let vernac_syntax_extension ~atts infix l =
let local = enforce_module_locality atts.locality in
if infix then Metasyntax.check_infix_modifiers (snd l);
Metasyntax.add_syntax_extension local l
-let vernac_delimiters sc = function
- | Some lr -> Metasyntax.add_delimiters sc lr
- | None -> Metasyntax.remove_delimiters sc
+let vernac_declare_scope ~atts sc =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.declare_scope local sc
+
+let vernac_delimiters ~atts sc action =
+ let local = enforce_module_locality atts.locality in
+ match action with
+ | Some lr -> Metasyntax.add_delimiters local sc lr
+ | None -> Metasyntax.remove_delimiters local sc
-let vernac_bind_scope sc cll =
- Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
+let vernac_bind_scope ~atts sc cll =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll)
let vernac_open_close_scope ~atts (b,s) =
let local = enforce_section_locality atts.locality in
@@ -548,7 +555,7 @@ let should_treat_as_uniform () =
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
-let vernac_record cum k poly finite records =
+let vernac_record ~template cum k poly finite records =
let is_cumulative = should_treat_as_cumulative cum poly in
let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
let const = match nameopt with
@@ -570,7 +577,7 @@ let vernac_record cum k poly finite records =
coe, id, pl, binders, cfs, const, sort
in
let records = List.map map records in
- ignore(Record.definition_structure k is_cumulative poly finite records)
+ ignore(Record.definition_structure ~template k is_cumulative poly finite records)
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
@@ -599,13 +606,14 @@ let vernac_inductive ~atts cum lo finite indl =
| [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
+ let template = atts.template in
if Option.has_some is_defclass then
(** Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
- vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+ vernac_record ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(** Mutual record case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -628,7 +636,7 @@ let vernac_inductive ~atts cum lo finite indl =
let ((_, _, _, kind, _), _) = List.hd indl in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
- vernac_record cum kind atts.polymorphic finite recordl
+ vernac_record ~template cum kind atts.polymorphic finite recordl
else if List.for_all is_constructor indl then
(** Mutual inductive case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -654,7 +662,7 @@ let vernac_inductive ~atts cum lo finite indl =
let indl = List.map unpack indl in
let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
let uniform = should_treat_as_uniform () in
- ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite
+ ComInductive.do_mutual_inductive ~template indl is_cumulative atts.polymorphic lo ~uniform finite
else
user_err (str "Mixed record-inductive definitions are not allowed")
(*
@@ -1802,13 +1810,13 @@ let vernac_print ~atts env sigma =
| PrintName (qid,udecl) ->
dump_global qid;
print_name env sigma qid udecl
- | PrintGraph -> Prettyp.print_graph env sigma
+ | PrintGraph -> Prettyp.print_graph ()
| PrintClasses -> Prettyp.print_classes()
| PrintTypeClasses -> Prettyp.print_typeclasses()
| PrintInstances c -> Prettyp.print_instances (smart_global c)
- | PrintCoercions -> Prettyp.print_coercions env sigma
+ | PrintCoercions -> Prettyp.print_coercions ()
| PrintCoercionPaths (cls,clt) ->
- Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)
+ Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
| PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
| PrintUniverses (b, dst) ->
let univ = Global.universes () in
@@ -2093,9 +2101,10 @@ let interp ?proof ~atts ~st c =
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
- vernac_syntax_extension atts infix sl
- | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
- | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
+ vernac_syntax_extension ~atts infix sl
+ | VernacDeclareScope sc -> vernac_declare_scope ~atts sc
+ | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr
+ | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl
| VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
| VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
| VernacNotation (c,infpl,sc) ->
@@ -2232,6 +2241,7 @@ let check_vernac_supports_locality c l =
| Some _, (
VernacOpenCloseScope _
| VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+ | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
| VernacDeclareCustomEntry _
| VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
| VernacAssumption _ | VernacStartTheoremProof _
@@ -2349,6 +2359,14 @@ let attributes_of_flags f atts =
(Some false, atts)
| ("polymorphic" | "monomorphic") ->
user_err Pp.(str "Polymorphism specified twice")
+ | "template" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some true }
+ | "notemplate" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some false }
+ | "template" | "notemplate" ->
+ user_err Pp.(str "Templateness specified twice")
| "local" when Option.is_empty atts.locality ->
assert_empty k v;
(polymorphism, { atts with locality = Some true })
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8fb74e6d78..11b2a7d802 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -325,6 +325,7 @@ type nonrec vernac_expr =
(* Syntax *)
| VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
| VernacOpenCloseScope of bool * scope_name
+ | VernacDeclareScope of scope_name
| VernacDelimiters of scope_name * string option
| VernacBindScope of scope_name * class_rawexpr list
| VernacInfix of (lstring * syntax_modifier list) *
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1bb1414f3d..2746cbd144 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,12 +21,13 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
- { loc ; locality ; polymorphic ; program ; deprecated }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
+ { loc ; locality ; polymorphic ; program ; deprecated; template }
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 46468b3098..62a178b555 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -18,12 +18,14 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
- ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+ ?polymorphic: bool -> ?template:bool option ->
+ ?program: bool -> ?deprecated: deprecation option -> unit -> atts
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:36:43 +0000