aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/canonical.ml39
-rw-r--r--vernac/canonical.mli12
-rw-r--r--vernac/class.ml53
-rw-r--r--vernac/classes.ml328
-rw-r--r--vernac/classes.mli22
-rw-r--r--vernac/comAssumption.ml102
-rw-r--r--vernac/comAssumption.mli20
-rw-r--r--vernac/comFixpoint.ml25
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comProgramFixpoint.ml32
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/himsg.ml8
-rw-r--r--vernac/indschemes.ml4
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/ppvernac.ml21
-rw-r--r--vernac/proof_using.ml3
-rw-r--r--vernac/proof_using.mli3
-rw-r--r--vernac/record.ml49
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernac.mllib3
-rw-r--r--vernac/vernacentries.ml29
-rw-r--r--vernac/vernacexpr.ml15
23 files changed, 582 insertions, 216 deletions
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
new file mode 100644
index 0000000000..92d5731f92
--- /dev/null
+++ b/vernac/canonical.ml
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+open Names
+open Libobject
+open Recordops
+
+let open_canonical_structure i (_, o) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
+
+let cache_canonical_structure (_, o) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ register_canonical_structure ~warn:true env sigma o
+
+let discharge_canonical_structure (_,x) = Some x
+
+let inCanonStruc : Constant.t * inductive -> obj =
+ declare_object {(default_object "CANONICAL-STRUCTURE") with
+ open_function = open_canonical_structure;
+ cache_function = cache_canonical_structure;
+ subst_function = (fun (subst,c) -> subst_canonical_structure subst c);
+ classify_function = (fun x -> Substitute x);
+ discharge_function = discharge_canonical_structure }
+
+let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
+
+let declare_canonical_structure ref =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ add_canonical_structure (check_and_decompose_canonical_structure env sigma ref)
diff --git a/vernac/canonical.mli b/vernac/canonical.mli
new file mode 100644
index 0000000000..5b223a0615
--- /dev/null
+++ b/vernac/canonical.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+open Names
+
+val declare_canonical_structure : GlobRef.t -> unit
diff --git a/vernac/class.ml b/vernac/class.ml
index 0837beccee..f3a279eab1 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -23,6 +23,7 @@ open Classops
open Declare
open Globnames
open Decl_kinds
+open Libobject
let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
@@ -230,6 +231,58 @@ let check_source = function
| Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s))
| _ -> ()
+let cache_coercion (_,c) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Classops.declare_coercion env sigma c
+
+let open_coercion i o =
+ if Int.equal i 1 then
+ cache_coercion o
+
+let discharge_coercion (_, c) =
+ if c.coercion_local then None
+ else
+ let n =
+ try
+ let ins = Lib.section_instance c.coercion_type in
+ Array.length (snd ins)
+ with Not_found -> 0
+ in
+ let nc = { c with
+ coercion_params = n + c.coercion_params;
+ coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
+ } in
+ Some nc
+
+let classify_coercion obj =
+ if obj.coercion_local then Dispose else Substitute obj
+
+let inCoercion : coercion -> obj =
+ declare_object {(default_object "COERCION") with
+ open_function = open_coercion;
+ cache_function = cache_coercion;
+ subst_function = (fun (subst,c) -> subst_coercion subst c);
+ classify_function = classify_coercion;
+ discharge_function = discharge_coercion }
+
+let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
+ let isproj =
+ match coef with
+ | ConstRef c -> Recordops.find_primitive_projection c
+ | _ -> None
+ in
+ let c = {
+ coercion_type = coef;
+ coercion_local = local;
+ coercion_is_id = isid;
+ coercion_is_proj = isproj;
+ coercion_source = cls;
+ coercion_target = clt;
+ coercion_params = ps;
+ } in
+ Lib.add_anonymous_leaf (inCoercion c)
+
(*
nom de la fonction coercion
strength de f
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d61d324941..9f233a2551 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -22,8 +22,10 @@ open Constrintern
open Constrexpr
open Context.Rel.Declaration
open Class_tactics
+open Libobject
module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
(*i*)
open Decl_kinds
@@ -49,17 +51,224 @@ let classes_transparent_state () =
with Not_found -> TransparentState.empty
let () =
- Hook.set Typeclasses.add_instance_hint_hook
- (fun inst path local info poly ->
+ Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
+ Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
+
+let add_instance_hint inst path local info poly =
let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
| IsGlobal gr -> Hints.IsGlobRef gr
in
Flags.silently (fun () ->
Hints.add_hints ~local [typeclasses_db]
(Hints.HintsResolveEntry
- [info, poly, false, Hints.PathHints path, inst'])) ());
- Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
- Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
+ [info, poly, false, Hints.PathHints path, inst'])) ()
+
+let is_local_for_hint i =
+ match i.is_global with
+ | None -> true (* i.e. either no Global keyword not in section, or in section *)
+ | Some n -> n <> 0 (* i.e. in a section, declare the hint as local
+ since discharge is managed by rebuild_instance which calls again
+ add_instance_hint; don't ask hints to take discharge into account
+ itself *)
+
+let add_instance check inst =
+ let poly = Global.is_polymorphic inst.is_impl in
+ let local = is_local_for_hint inst in
+ add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
+ inst.is_info poly;
+ List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
+ local pri poly)
+ (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
+ (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
+
+let mk_instance cl info glob impl =
+ let global =
+ if glob then Some (Lib.sections_depth ())
+ else None
+ in
+ if match global with Some n -> n>0 && isVarRef impl | _ -> false then
+ CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable.");
+ { is_class = cl.cl_impl;
+ is_info = info ;
+ is_global = global ;
+ is_impl = impl }
+
+(*
+ * instances persistent object
+ *)
+let cache_instance (_, i) =
+ load_instance i
+
+let subst_instance (subst, inst) =
+ { inst with
+ is_class = fst (subst_global subst inst.is_class);
+ is_impl = fst (subst_global subst inst.is_impl) }
+
+let discharge_instance (_, inst) =
+ match inst.is_global with
+ | None -> None
+ | Some n ->
+ assert (not (isVarRef inst.is_impl));
+ Some
+ { inst with
+ is_global = Some (pred n);
+ is_class = inst.is_class;
+ is_impl = inst.is_impl }
+
+let is_local i = (i.is_global == None)
+
+let rebuild_instance inst =
+ add_instance true inst;
+ inst
+
+let classify_instance inst =
+ if is_local inst then Dispose
+ else Substitute inst
+
+let instance_input : instance -> obj =
+ declare_object
+ { (default_object "type classes instances state") with
+ cache_function = cache_instance;
+ load_function = (fun _ x -> cache_instance x);
+ open_function = (fun _ x -> cache_instance x);
+ classify_function = classify_instance;
+ discharge_function = discharge_instance;
+ rebuild_function = rebuild_instance;
+ subst_function = subst_instance }
+
+let add_instance i =
+ Lib.add_anonymous_leaf (instance_input i);
+ add_instance true i
+
+let warning_not_a_class =
+ let name = "not-a-class" in
+ let category = "typeclasses" in
+ CWarnings.create ~name ~category (fun (n, ty) ->
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ Pp.(str "Ignored instance declaration for “"
+ ++ Nametab.pr_global_env Id.Set.empty n
+ ++ str "”: “"
+ ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
+ ++ str "” is not a class")
+ )
+
+let declare_instance ?(warn = false) env sigma info local glob =
+ let ty, _ = Typeops.type_of_global_in_context env glob in
+ let info = Option.default {hint_priority = None; hint_pattern = None} info in
+ match class_of_constr env sigma (EConstr.of_constr ty) with
+ | Some (rels, ((tc,_), args) as _cl) ->
+ assert (not (isVarRef glob) || local);
+ add_instance (mk_instance tc info (not local) glob)
+ | None -> if warn then warning_not_a_class (glob, ty)
+
+(*
+ * classes persistent object
+ *)
+
+let cache_class (_,c) = load_class c
+
+let subst_class (subst,cl) =
+ let do_subst_con c = Mod_subst.subst_constant subst c
+ and do_subst c = Mod_subst.subst_mps subst c
+ and do_subst_gr gr = fst (subst_global subst gr) in
+ let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
+ let do_subst_context (grs,ctx) =
+ List.Smart.map (Option.Smart.map do_subst_gr) grs,
+ do_subst_ctx ctx in
+ let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
+ (x, y, Option.Smart.map do_subst_con z)) projs in
+ { cl_univs = cl.cl_univs;
+ cl_impl = do_subst_gr cl.cl_impl;
+ cl_context = do_subst_context cl.cl_context;
+ cl_props = do_subst_ctx cl.cl_props;
+ cl_projs = do_subst_projs cl.cl_projs;
+ cl_strict = cl.cl_strict;
+ cl_unique = cl.cl_unique }
+
+let discharge_class (_,cl) =
+ let open CVars in
+ let repl = Lib.replacement_context () in
+ let rel_of_variable_context ctx = List.fold_right
+ ( fun (decl,_) (ctx', subst) ->
+ let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
+ (decl' :: ctx', NamedDecl.get_id decl :: subst)
+ ) ctx ([], []) in
+ let discharge_rel_context (subst, usubst) n rel =
+ let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
+ let fold decl (ctx, k) =
+ let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
+ RelDecl.map_constr map decl :: ctx, succ k
+ in
+ let ctx, _ = List.fold_right fold rel ([], n) in
+ ctx
+ in
+ let abs_context cl =
+ match cl.cl_impl with
+ | VarRef _ | ConstructRef _ -> assert false
+ | ConstRef cst -> Lib.section_segment_of_constant cst
+ | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
+ let discharge_context ctx' subst (grs, ctx) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let grs' =
+ let newgrs = List.map (fun decl ->
+ match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with
+ | None -> None
+ | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
+ ctx'
+ in
+ grs @ newgrs
+ in grs', discharge_rel_context subst 1 ctx @ ctx' in
+ try
+ let info = abs_context cl in
+ let ctx = info.Lib.abstr_ctx in
+ let ctx, subst = rel_of_variable_context ctx in
+ let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
+ let context = discharge_context ctx (subst, usubst) cl.cl_context in
+ let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
+ let discharge_proj x = x in
+ { cl_univs = cl_univs';
+ cl_impl = cl.cl_impl;
+ cl_context = context;
+ cl_props = props;
+ cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+ cl_strict = cl.cl_strict;
+ cl_unique = cl.cl_unique
+ }
+ with Not_found -> (* not defined in the current section *)
+ cl
+
+let rebuild_class cl =
+ try
+ let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
+ set_typeclass_transparency cst false false; cl
+ with e when CErrors.noncritical e -> cl
+
+let class_input : typeclass -> obj =
+ declare_object
+ { (default_object "type classes state") with
+ cache_function = cache_class;
+ load_function = (fun _ -> cache_class);
+ open_function = (fun _ -> cache_class);
+ classify_function = (fun x -> Substitute x);
+ discharge_function = (fun a -> Some (discharge_class a));
+ rebuild_function = rebuild_class;
+ subst_function = subst_class }
+
+let add_class cl =
+ Lib.add_anonymous_leaf (class_input cl)
+
+let add_class env sigma cl =
+ add_class cl;
+ List.iter (fun (n, inst, body) ->
+ match inst with
+ | Some (Backward, info) ->
+ (match body with
+ | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
+ | Some b -> declare_instance ~warn:true env sigma (Some info) false (ConstRef b))
+ | _ -> ())
+ cl.cl_projs
let intern_info {hint_priority;hint_pattern} =
let env = Global.env() in
@@ -72,10 +281,12 @@ let existing_instance glob g info =
let c = Nametab.global g in
let info = Option.default Hints.empty_hint_info info in
let info = intern_info info in
- let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ let instance, _ = Typeops.type_of_global_in_context env c in
let _, r = Term.decompose_prod_assum instance in
- match class_of_constr Evd.empty (EConstr.of_constr r) with
- | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
+ match class_of_constr env sigma (EConstr.of_constr r) with
+ | Some (_, ((tc,u), _)) -> add_instance (mk_instance tc info glob c)
| None -> user_err ?loc:g.CAst.loc
~hdr:"declare_instance"
(Pp.str "Constant does not build instances of a declared type class.")
@@ -111,7 +322,9 @@ let id_of_class cl =
let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst imps;
let info = intern_info info in
- Typeclasses.declare_instance (Some info) (not global) cst;
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ declare_instance env sigma (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
@@ -154,7 +367,9 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr imps;
let pri = intern_info pri in
- Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ declare_instance env sigma (Some pri) (not global) (ConstRef cst)
in
let obls, constr, typ =
match term with
@@ -360,96 +575,3 @@ let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl)
interp_instance_context ~program_mode env ctx pl bk cl
in
do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
-
-let named_of_rel_context l =
- let open Vars in
- let acc, ctx =
- List.fold_right
- (fun decl (subst, ctx) ->
- let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
- let d = match decl with
- | LocalAssum (_,t) -> id, None, substl subst t
- | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
- (mkVar id :: subst, d :: ctx))
- l ([], [])
- in ctx
-
-let context ~pstate poly l =
- let env = Global.env() in
- let sigma = Evd.from_env env in
- let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
- (* Note, we must use the normalized evar from now on! *)
- let sigma = Evd.minimize_universes sigma in
- let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
- let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
- let ctx =
- try named_of_rel_context fullctx
- with e when CErrors.noncritical e ->
- user_err Pp.(str "Anonymous variables not allowed in contexts.")
- in
- let univs =
- match ctx with
- | [] -> assert false
- | [_] -> Evd.univ_entry ~poly sigma
- | _::_::_ ->
- if Lib.sections_are_opened ()
- then
- (* More than 1 variable in a section: we can't associate
- universes to any specific variable so we declare them
- separately. *)
- begin
- let uctx = Evd.universe_context_set sigma in
- Declare.declare_universe_context poly uctx;
- if poly then Polymorphic_entry ([||], Univ.UContext.empty)
- else Monomorphic_entry Univ.ContextSet.empty
- end
- else if poly then
- (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
- Evd.univ_entry ~poly sigma
- else
- (* Multiple monomorphic axioms: declare universes separately
- to avoid redeclaring them. *)
- begin
- let uctx = Evd.universe_context_set sigma in
- Declare.declare_universe_context poly uctx;
- Monomorphic_entry Univ.ContextSet.empty
- end
- in
- let fn status (id, b, t) =
- let b, t = Option.map (to_constr sigma) b, to_constr sigma t in
- if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
- (* Declare the universe context once *)
- let decl = match b with
- | None ->
- (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
- | Some b ->
- let entry = Declare.definition_entry ~univs ~types:t b in
- (DefinitionEntry entry, IsAssumption Logical)
- in
- let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
- match class_of_constr sigma (of_constr t) with
- | Some (rels, ((tc,_), args) as _cl) ->
- add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
- status
- (* declare_subclasses (ConstRef cst) cl *)
- | None -> status
- else
- let test (x, _) = match x with
- | ExplByPos (_, Some id') -> Id.equal id id'
- | _ -> false
- in
- let impl = List.exists test impls in
- let decl = (Discharge, poly, Definitional) in
- let nstatus = match b with
- | None ->
- pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
- Declaremods.NoInline (CAst.make id))
- | Some b ->
- let decl = (Discharge, poly, Definition) in
- let entry = Declare.definition_entry ~univs ~types:t b in
- let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
- Lib.sections_are_opened () || Lib.is_modtype_strict ()
- in
- status && nstatus
- in
- List.fold_left fn true (List.rev ctx)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 73e4b024ef..e7f90ff306 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,6 +22,12 @@ val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
(** Instance declaration *)
+val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
+ hint_info option -> bool -> GlobRef.t -> unit
+(** Declares the given global reference as an instance of its type.
+ Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
+ when said type is not a registered type class. *)
+
val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
@@ -64,6 +70,12 @@ val declare_new_instance :
Hints.hint_info_expr ->
unit
+(** {6 Low level interface used by Add Morphism, do not use } *)
+val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
+val add_instance : instance -> unit
+
+val add_class : env -> Evd.evar_map -> typeclass -> unit
+
(** Setting opacity *)
val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -71,13 +83,3 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
(** For generation on names based on classes only *)
val id_of_class : typeclass -> Id.t
-
-(** Context command *)
-
-(** returns [false] if, for lack of section, it declares an assumption
- (unless in a module type). *)
-val context
- : pstate:Proof_global.t option
- -> Decl_kinds.polymorphic
- -> local_binder_expr list
- -> bool
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d7bd64067b..3406b6276f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -22,6 +22,7 @@ open Decl_kinds
open Pretyping
open Entries
+module RelDecl = Context.Rel.Declaration
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
let axiom_into_instance = ref false
@@ -59,7 +60,9 @@ match local with
in
let r = VarRef ident in
let () = maybe_declare_manual_implicits true r imps in
- let () = Typeclasses.declare_instance None true r in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let () = Classes.declare_instance env sigma None true r in
let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,Univ.Instance.empty,true)
@@ -77,7 +80,9 @@ match local with
let () = maybe_declare_manual_implicits false gr imps in
let () = Declare.declare_univ_binders gr pl in
let () = assumption_message ident in
- let () = if do_instance then Typeclasses.declare_instance None false gr in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let () = if do_instance then Classes.declare_instance env sigma None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
let inst = match ctx with
| Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
@@ -173,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l =
let ubinders = Evd.universe_binders sigma in
pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
- let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in
+ let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
(fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
idl refs
@@ -206,3 +211,94 @@ let do_primitive id prim typopt =
in
let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
+
+let named_of_rel_context l =
+ let open EConstr.Vars in
+ let open RelDecl in
+ let acc, ctx =
+ List.fold_right
+ (fun decl (subst, ctx) ->
+ let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+ let d = match decl with
+ | LocalAssum (_,t) -> id, None, substl subst t
+ | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+ (EConstr.mkVar id :: subst, d :: ctx))
+ l ([], [])
+ in ctx
+
+let context ~pstate poly l =
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
+ (* Note, we must use the normalized evar from now on! *)
+ let sigma = Evd.minimize_universes sigma in
+ let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
+ let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
+ let ctx =
+ try named_of_rel_context fullctx
+ with e when CErrors.noncritical e ->
+ user_err Pp.(str "Anonymous variables not allowed in contexts.")
+ in
+ let univs =
+ match ctx with
+ | [] -> assert false
+ | [_] -> Evd.univ_entry ~poly sigma
+ | _::_::_ ->
+ if Lib.sections_are_opened ()
+ then
+ (* More than 1 variable in a section: we can't associate
+ universes to any specific variable so we declare them
+ separately. *)
+ begin
+ let uctx = Evd.universe_context_set sigma in
+ Declare.declare_universe_context poly uctx;
+ if poly then Polymorphic_entry ([||], Univ.UContext.empty)
+ else Monomorphic_entry Univ.ContextSet.empty
+ end
+ else if poly then
+ (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
+ Evd.univ_entry ~poly sigma
+ else
+ (* Multiple monomorphic axioms: declare universes separately
+ to avoid redeclaring them. *)
+ begin
+ let uctx = Evd.universe_context_set sigma in
+ Declare.declare_universe_context poly uctx;
+ Monomorphic_entry Univ.ContextSet.empty
+ end
+ in
+ let fn status (id, b, t) =
+ let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
+ if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
+ (* Declare the universe context once *)
+ let decl = match b with
+ | None ->
+ (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
+ | Some b ->
+ let entry = Declare.definition_entry ~univs ~types:t b in
+ (DefinitionEntry entry, IsAssumption Logical)
+ in
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
+ let env = Global.env () in
+ Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
+ status
+ else
+ let test (x, _) = match x with
+ | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+ | _ -> false
+ in
+ let impl = List.exists test impls in
+ let decl = (Discharge, poly, Definitional) in
+ let nstatus = match b with
+ | None ->
+ pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
+ Declaremods.NoInline (CAst.make id))
+ | Some b ->
+ let decl = (Discharge, poly, Definition) in
+ let entry = Declare.definition_entry ~univs ~types:t b in
+ let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
+ Lib.sections_are_opened () || Lib.is_modtype_strict ()
+ in
+ status && nstatus
+ in
+ List.fold_left fn true (List.rev ctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 32914cc11b..7c64317b70 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -9,8 +9,6 @@
(************************************************************************)
open Names
-open Constr
-open Entries
open Vernacexpr
open Constrexpr
open Decl_kinds
@@ -25,19 +23,13 @@ val do_assumptions
-> (ident_decl list * constr_expr) with_coercion list
-> bool
-(************************************************************************)
-(** Internal API *)
-(************************************************************************)
-
-(** Exported for Classes *)
-
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
val declare_assumption
: pstate:Proof_global.t option
-> coercion_flag
-> assumption_kind
- -> types in_universes_entry
+ -> Constr.types Entries.in_universes_entry
-> UnivNames.universe_binders
-> Impargs.manual_implicits
-> bool (** implicit *)
@@ -45,4 +37,14 @@ val declare_assumption
-> variable CAst.t
-> GlobRef.t * Univ.Instance.t * bool
+(** Context command *)
+
+(** returns [false] if, for lack of section, it declares an assumption
+ (unless in a module type). *)
+val context
+ : pstate:Proof_global.t option
+ -> Decl_kinds.polymorphic
+ -> local_binder_expr list
+ -> bool
+
val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2aadbd224f..1912646ffd 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
pstate
-let extract_decreasing_argument limit = function
- | (na,CStructRec) -> na
- | (na,_) when not limit -> na
+let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
+ | CStructRec na -> na
+ | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
+ | CMeasureRec (None,_,_) when not structonly ->
+ user_err Pp.(str "Decreasing argument must be specificed in measure clause.")
| _ -> user_err Pp.(str
- "Only structural decreasing is supported for a non-Program Fixpoint")
+ "Well-founded induction requires Program Fixpoint or Function.")
-let extract_fixpoint_components limit l =
+let extract_fixpoint_components ~structonly l =
let fixl, ntnl = List.split l in
let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
- let ann = extract_decreasing_argument limit ann in
+ (* This is a special case: if there's only one binder, we pick it as the
+ recursive argument if none is provided. *)
+ let ann = Option.map (fun ann -> match bl, ann with
+ | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | _, x -> x) ann
+ in
+ let ann = Option.map (extract_decreasing_argument ~structonly) ann in
{fix_name = id; fix_annot = ann; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
fixl, List.flatten ntnl
@@ -356,7 +367,7 @@ let check_safe () =
flags.check_universes && flags.check_guarded
let do_fixpoint ~ontop local poly l =
- let fixl, ntns = extract_fixpoint_components true l in
+ let fixl, ntns = extract_fixpoint_components ~structonly:true l in
let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 15ff5f4498..5937842f17 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -62,7 +62,7 @@ val interp_recursive :
(** Extracting the semantical components out of the raw syntax of
(co)fixpoints declarations *)
-val extract_fixpoint_components : bool ->
+val extract_fixpoint_components : structonly:bool ->
(fixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 350b2d2945..20a2db7ca2 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -85,7 +85,7 @@ let rec telescope sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- let recarg =
- match n with
- | Some n -> mkIdentC n.CAst.v
- | None ->
- user_err ~hdr:"do_program_fixpoint"
- (str "Recursive argument required for well-founded fixpoints")
- in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
+ | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ let recarg = mkIdentC n.CAst.v in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
- | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- build_wellfounded (id, pl, n, bl, typ, out_def def) poly
+ | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *)
+ let r = match n, r with
+ | Some id, None ->
+ let loc = id.CAst.loc in
+ Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None))
+ | Some _, Some _ ->
+ user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
+ | _, _ -> r
+ in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
- | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
- let fixl,ntns = extract_fixpoint_components true l in
- let fixkind = Obligations.IsFixpoint g in
+ | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
+ let fixl,ntns = extract_fixpoint_components ~structonly:true l in
+ let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1533d0ccd3..3f491d1dd4 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram
GLOBAL: command query_command class_rawexpr gallina_ext;
gallina_ext:
- [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
+ [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (true, table, v) }
| IDENT "Export"; IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (true, table) }
+ { VernacSetOption (true, table, OptionUnset) }
] ];
command:
@@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram
{ VernacAddMLPath (true, dir) }
(* For acting on parameter tables *)
- | "Set"; table = option_table; v = option_value ->
+ | "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (false, table, v) }
| IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (false, table) }
+ { VernacSetOption (false, table, OptionUnset) }
| IDENT "Print"; IDENT "Table"; table = option_table ->
{ VernacPrintOption table }
@@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram
| IDENT "Library"; qid = global -> { LocateLibrary qid }
| IDENT "Module"; qid = global -> { LocateModule qid } ] ]
;
- option_value:
- [ [ -> { BoolValue true }
- | n = integer -> { IntValue (Some n) }
- | s = STRING -> { StringValue s } ] ]
+ option_setting:
+ [ [ -> { OptionSetTrue }
+ | n = integer -> { OptionSetInt n }
+ | s = STRING -> { OptionSetString s } ] ]
;
option_ref_value:
[ [ id = global -> { QualidRefValue id }
@@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) }
| IDENT "Debug"; IDENT "Off" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) }
(* registration of a custom reduction *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 32754478a5..082b22b373 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -601,7 +601,7 @@ let rec explain_evar_kind env sigma evk ty =
(pr_leconstr_env env sigma ty') src
let explain_typeclass_resolution env sigma evi k =
- match Typeclasses.class_of_constr sigma evi.evar_concl with
+ match Typeclasses.class_of_constr env sigma evi.evar_concl with
| Some _ ->
let env = Evd.evar_filtered_env evi in
fnl () ++ str "Could not find an instance for " ++
@@ -614,7 +614,7 @@ let explain_placeholder_kind env sigma c e =
| Some (SeveralInstancesFound n) ->
strbrk " (several distinct possible type class instances found)"
| None ->
- match Typeclasses.class_of_constr sigma c with
+ match Typeclasses.class_of_constr env sigma c with
| Some _ -> strbrk " (no type class instance found)"
| _ -> mt ()
@@ -731,7 +731,9 @@ let explain_undeclared_universe env sigma l =
spc () ++ str "(maybe a bugged tactic)."
let explain_disallowed_sprop () =
- Pp.(str "SProp not allowed, you need to use -allow-sprop.")
+ Pp.(strbrk "SProp not allowed, you need to "
+ ++ str "Set Allow StrictProp"
+ ++ strbrk " or to use the -allow-sprop command-line-flag.")
let explain_bad_relevance env =
strbrk "Bad relevance (maybe a bugged tactic)."
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 1e733acc59..642695bda4 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -313,7 +313,9 @@ let warn_cannot_build_congruence =
strbrk "Cannot build congruence scheme because eq is not found")
let declare_congr_scheme ind =
- if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ if Hipattern.is_equality_type env sigma (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin
if
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 07194578c1..1b1c618dc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,7 +295,7 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -486,7 +486,7 @@ let rec lam_index n t acc =
lam_index n b (succ acc)
| _ -> raise Not_found
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
+let compute_possible_guardness_evidences n fixbody fixtype =
match n with
| Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
| None ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1b7b1ec90..d25daeed9c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -70,7 +70,7 @@ type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b602e134da..4e4d431e89 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -173,15 +173,10 @@ open Pputils
pr_opt (prlist_with_sep sep pr_option_ref_value) b
let pr_set_option a b =
- let pr_opt_value = function
- | IntValue None -> assert false
- (* This should not happen because of the grammar *)
- | IntValue (Some n) -> spc() ++ int n
- | StringValue s -> spc() ++ str s
- | StringOptValue None -> mt()
- | StringOptValue (Some s) -> spc() ++ str s
- | BoolValue b -> mt()
- in pr_printoption a None ++ pr_opt_value b
+ pr_printoption a None ++ (match b with
+ | OptionUnset | OptionSetTrue -> mt()
+ | OptionSetInt n -> spc() ++ int n
+ | OptionSetString s -> spc() ++ quote (str s))
let pr_opt_hintbases l = match l with
| [] -> mt()
@@ -1140,15 +1135,11 @@ open Pputils
hov 1 (keyword "Strategy" ++ spc() ++
hv 0 (prlist_with_sep sep pr_line l))
)
- | VernacUnsetOption (export, na) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- return (
- hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
- )
| VernacSetOption (export, na,v) ->
let export = if export then keyword "Export" ++ spc () else mt () in
+ let set = if v == OptionUnset then "Unset" else "Set" in
return (
- hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
+ hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
)
| VernacAddOption (na,l) ->
return (
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 526845084a..1d089d0a55 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -172,11 +172,12 @@ let value = ref None
let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
+let proof_using_opt_name = ["Default";"Proof";"Using"]
let () =
Goptions.(declare_stringopt_option
{ optdepr = false;
optname = "default value for Proof using";
- optkey = ["Default";"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/proof_using.mli b/vernac/proof_using.mli
index 7d1110aaa2..702043a4a9 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit
val suggest_variable : Environ.env -> Names.Id.t -> unit
val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
+
+val proof_using_opt_name : string list
+(** For the stm *)
diff --git a/vernac/record.ml b/vernac/record.ml
index cb67548667..74e5a03659 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -30,6 +30,7 @@ open Constrexpr
open Constrexpr_ops
open Goptions
open Context.Rel.Declaration
+open Libobject
module RelDecl = Context.Rel.Declaration
@@ -373,6 +374,27 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
open Typeclasses
+let load_structure i (_, structure) =
+ Recordops.register_structure (Global.env()) structure
+
+let cache_structure o =
+ load_structure 1 o
+
+let subst_structure (subst, (id, kl, projs as obj)) =
+ Recordops.subst_structure subst obj
+
+let discharge_structure (_, x) = Some x
+
+let inStruc : Recordops.struc_tuple -> obj =
+ declare_object {(default_object "STRUCTURE") with
+ cache_function = cache_structure;
+ load_function = load_structure;
+ subst_function = subst_structure;
+ classify_function = (fun x -> Substitute x);
+ discharge_function = discharge_structure }
+
+let declare_structure_entry o =
+ Lib.add_anonymous_leaf (inStruc o)
let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
let nparams = List.length params in
@@ -443,7 +465,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
- let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
+ let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
List.mapi map record_data
@@ -520,8 +542,10 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
List.map map inds
in
let ctx_context =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
List.map (fun decl ->
- match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
+ match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with
| Some (_, ((cl,_), _)) -> Some cl.cl_impl
| None -> None)
params, params
@@ -548,12 +572,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
cl_props = fields;
cl_projs = projs }
in
- add_class k; impl
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Classes.add_class env sigma k; impl
in
List.map map data
-let add_constant_class env cst =
+let add_constant_class env sigma cst =
let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
let r = (Environ.lookup_constant cst env).const_relevance in
let ctx, arity = decompose_prod_assum ty in
@@ -566,10 +592,11 @@ let add_constant_class env cst =
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique
}
- in add_class tc;
+ in
+ Classes.add_class env sigma tc;
set_typeclass_transparency (EvalConstRef cst) false false
-
-let add_inductive_class env ind =
+
+let add_inductive_class env sigma ind =
let mind, oneind = Inductive.lookup_mind_specif env ind in
let k =
let ctx = oneind.mind_arity_ctxt in
@@ -586,7 +613,8 @@ let add_inductive_class env ind =
cl_projs = [];
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique }
- in add_class k
+ in
+ Classes.add_class env sigma k
let warn_already_existing_class =
CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
@@ -594,11 +622,12 @@ let warn_already_existing_class =
let declare_existing_class g =
let env = Global.env () in
+ let sigma = Evd.from_env env in
if Typeclasses.is_class g then warn_already_existing_class g
else
match g with
- | ConstRef x -> add_constant_class env x
- | IndRef x -> add_inductive_class env x
+ | ConstRef x -> add_constant_class env sigma x
+ | IndRef x -> add_inductive_class env sigma x
| _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
diff --git a/vernac/record.mli b/vernac/record.mli
index 9852840d12..12a2a765b5 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,6 +24,8 @@ val declare_projections :
Constr.rel_context ->
(Name.t * bool) list * Constant.t option list
+val declare_structure_entry : Recordops.struc_tuple -> unit
+
val definition_structure :
universe_decl_expr option -> inductive_kind -> template:bool option ->
Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index ce93a8baaf..7f5c265eea 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -12,6 +12,7 @@ Vernacextend
Ppvernac
Proof_using
Lemmas
+Canonical
Class
Egramcoq
Metasyntax
@@ -21,11 +22,11 @@ Indschemes
DeclareDef
Obligations
ComDefinition
+Classes
ComAssumption
ComInductive
ComFixpoint
ComProgramFixpoint
-Classes
Record
Assumptions
Vernacstate
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 02db75c0f9..3a305c3b61 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -572,7 +572,7 @@ let vernac_definition_hook p = function
| Coercion ->
Some (Class.add_coercion_hook p)
| CanonicalStructure ->
- Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
+ Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure))
| SubClass ->
Some (Class.add_subclass_hook p)
| _ -> None
@@ -1041,7 +1041,7 @@ let vernac_require from import qidl =
(* Coercions and canonical structures *)
let vernac_canonical r =
- Recordops.declare_canonical_structure (smart_global r)
+ Canonical.declare_canonical_structure (smart_global r)
let vernac_coercion ~atts ref qids qidt =
let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
@@ -1075,7 +1075,7 @@ let vernac_declare_instance ~atts sup inst pri =
Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
let vernac_context ~pstate ~poly l =
- if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
+ if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
let vernac_existing_instance ~section_local insts =
let glob = not section_local in
@@ -1096,7 +1096,10 @@ let focus_command_cond = Proof.no_cond command_focus
there are no more goals to solve. It cannot be a tactic since
all tactics fail if there are no further goals to prove. *)
-let vernac_solve_existential ~pstate i e = Pfedit.instantiate_nth_evar_com i e pstate
+let vernac_solve_existential ~pstate n com =
+ Proof_global.simple_with_current_proof (fun _ p ->
+ let intern env sigma = Constrintern.intern_constr env sigma com in
+ Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
let vernac_set_end_tac ~pstate tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
@@ -1704,18 +1707,17 @@ let get_option_locality export local =
let vernac_set_option0 ~local export key opt =
let locality = get_option_locality export local in
match opt with
- | StringValue s -> set_string_option_value_gen ~locality key s
- | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
- | StringOptValue None -> unset_option_value_gen ~locality key
- | IntValue n -> set_int_option_value_gen ~locality key n
- | BoolValue b -> set_bool_option_value_gen ~locality key b
+ | OptionUnset -> unset_option_value_gen ~locality key
+ | OptionSetString s -> set_string_option_value_gen ~locality key s
+ | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n)
+ | OptionSetTrue -> set_bool_option_value_gen ~locality key true
let vernac_set_append_option ~local export key s =
let locality = get_option_locality export local in
set_string_option_append_value_gen ~locality key s
let vernac_set_option ~local export table v = match v with
-| StringValue s ->
+| OptionSetString s ->
(* We make a special case for warnings because appending is their
natural semantics *)
if CString.List.equal table ["Warnings"] then
@@ -1728,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with
vernac_set_option0 ~local export table v
| _ -> vernac_set_option0 ~local export table v
-let vernac_unset_option ~local export key =
- let locality = get_option_locality export local in
- unset_option_value_gen ~locality key
-
let vernac_add_option key lv =
let f = function
| StringRefValue s -> (get_string_table key)#add s
@@ -2459,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
| VernacSetOption (export, key,v) ->
vernac_set_option ~local:(only_locality atts) export key v;
pstate
- | VernacUnsetOption (export, key) ->
- vernac_unset_option ~local:(only_locality atts) export key;
- pstate
| VernacRemoveOption (key,v) ->
unsupported_attributes atts;
vernac_remove_option key v;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ebfc473522..d0dae1aa53 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option
which this notation is trying to be compatible with *)
type locality_flag = bool (* true = Local *)
-type option_value = Goptions.option_value =
- | BoolValue of bool
- | IntValue of int option
- | StringValue of string
- | StringOptValue of string option
+type option_setting =
+ | OptionUnset
+ | OptionSetTrue
+ | OptionSetInt of int
+ | OptionSetString of string
type option_ref_value =
| StringRefValue of string
@@ -129,7 +129,7 @@ type definition_expr =
* constr_expr option
type fixpoint_expr =
- ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+ ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option
type cofixpoint_expr =
ident_decl * local_binder_expr list * constr_expr * constr_expr option
@@ -363,8 +363,7 @@ type nonrec vernac_expr =
| VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
| VernacSetStrategy of
(Conv_oracle.level * qualid or_by_notation list) list
- | VernacUnsetOption of export_flag * Goptions.option_name
- | VernacSetOption of export_flag * Goptions.option_name * option_value
+ | VernacSetOption of export_flag * Goptions.option_name * option_setting
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:53:49 +0000