aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common2
-rw-r--r--plugins/ltac/coretactics.ml48
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/g_eqdecide.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/tauto.ml3
-rw-r--r--plugins/ltac/tauto_plugin.mlpack1
-rw-r--r--stm/stm.ml22
-rw-r--r--test-suite/bugs/closed/3612.v1
-rw-r--r--test-suite/bugs/closed/3649.v2
-rw-r--r--theories/Init/Notations.v6
-rw-r--r--theories/Init/Tauto.v2
-rw-r--r--tools/coqdep_lexer.mll4
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/command.ml68
-rw-r--r--vernac/command.mli12
-rw-r--r--vernac/declareDef.ml64
-rw-r--r--vernac/declareDef.mli19
-rw-r--r--vernac/obligations.ml11
-rw-r--r--vernac/obligations.mli11
-rw-r--r--vernac/vernac.mllib1
24 files changed, 119 insertions, 131 deletions
diff --git a/Makefile.common b/Makefile.common
index ec5e6ac855..100698321a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -134,7 +134,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
ascii_syntax_plugin.cmo \
string_syntax_plugin.cmo )
DERIVECMO:=plugins/derive/derive_plugin.cmo
-LTACCMO:=plugins/ltac/ltac_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb2..50013f5583 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -17,7 +17,7 @@ open Stdarg
open Extraargs
open Names
-DECLARE PLUGIN "coretactics"
+DECLARE PLUGIN "ltac_plugin"
(** Basic tactics *)
@@ -324,11 +324,11 @@ let initial_atomic () =
"fresh", TacArg(Loc.tag @@ TacFreshId [])
]
-let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
(* First-class Ltac access to primitive blocks *)
-let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
let register_list_tactical name f =
@@ -356,4 +356,4 @@ let initial_tacticals () =
"solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
]
-let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
+let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7259faecd0..36df25cc77 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -28,7 +28,7 @@ open Equality
open Misctypes
open Proofview.Notations
-DECLARE PLUGIN "extratactics"
+DECLARE PLUGIN "ltac_plugin"
(**********************************************************************)
(* replace, discriminate, injection, simplify_eq *)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfd8e88a91..6145e373b1 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -18,7 +18,7 @@ open Pcoq.Constr
open Pltac
open Hints
-DECLARE PLUGIN "g_auto"
+DECLARE PLUGIN "ltac_plugin"
(* Hint bases *)
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 905cfd02a6..63451210ca 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,7 +13,7 @@ open Class_tactics
open Stdarg
open Tacarg
-DECLARE PLUGIN "g_class"
+DECLARE PLUGIN "ltac_plugin"
(** Options: depth, debug and transparency settings. *)
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 570cd4e694..dceefeaa13 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -17,7 +17,7 @@
open API
open Eqdecide
-DECLARE PLUGIN "g_eqdecide"
+DECLARE PLUGIN "ltac_plugin"
TACTIC EXTEND decide_equality
| [ "decide" "equality" ] -> [ decideEqualityGoal ]
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index e6ddc5cc1b..3e6f420065 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -27,7 +27,7 @@ open Pcoq.Prim
open Pcoq.Constr
open Pltac
-DECLARE PLUGIN "g_rewrite"
+DECLARE PLUGIN "ltac_plugin"
type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index af1c7149da..12b4c81fc4 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -21,7 +21,6 @@ G_auto
G_class
Rewrite
G_rewrite
-Tauto
G_eqdecide
G_tactic
G_ltac
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 2a8ed72387..71f7082e70 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,13 +13,14 @@ open Hipattern
open Names
open Geninterp
open Misctypes
+open Ltac_plugin
open Tacexpr
open Tacinterp
open Util
open Tacticals.New
open Proofview.Notations
-let tauto_plugin = "tauto"
+let tauto_plugin = "tauto_plugin"
let () = Mltop.add_known_module tauto_plugin
let assoc_var s ist =
diff --git a/plugins/ltac/tauto_plugin.mlpack b/plugins/ltac/tauto_plugin.mlpack
new file mode 100644
index 0000000000..b3618018ea
--- /dev/null
+++ b/plugins/ltac/tauto_plugin.mlpack
@@ -0,0 +1 @@
+Tauto
diff --git a/stm/stm.ml b/stm/stm.ml
index 071d2edf98..b9247fff04 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1672,7 +1672,7 @@ end (* }}} *)
and TacTask : sig
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
@@ -1681,13 +1681,12 @@ and TacTask : sig
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
- exception NoProgress
include AsyncTaskQueue.Task with type task := task
end = struct (* {{{ *)
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -1709,10 +1708,9 @@ end = struct (* {{{ *)
r_name : string }
type response =
- | RespBuiltSubProof of output
+ | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
| RespError of Pp.std_ppcmds
| RespNoProgress
- exception NoProgress
let name = ref "tacworker"
let extra_env () = [||]
@@ -1734,10 +1732,9 @@ end = struct (* {{{ *)
let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
match resp with
- | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+ | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
| RespNoProgress ->
- let e = (NoProgress, Exninfo.null) in
- t_assign (`Exn e);
+ t_assign (`Val None);
t_kill ();
`Stay ((),[])
| RespError msg ->
@@ -1848,8 +1845,8 @@ end = struct (* {{{ *)
else tclUNIT ()
else
let open Notations in
- try
- let pt, uc = Future.join f in
+ match Future.join f with
+ | Some (pt, uc) ->
stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
@@ -1857,7 +1854,7 @@ end = struct (* {{{ *)
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
Tactics.exact_no_check (EConstr.of_constr pt))
- with TacTask.NoProgress ->
+ | None ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
end)
in
@@ -2523,11 +2520,12 @@ let process_transaction ?(newtip=Stateid.fresh ())
| VtQuery (false, route), VtNow ->
begin
let query_sid = VCS.cur_tip () in
- try stm_vernac_interp (VCS.cur_tip ()) x
+ try stm_vernac_interp ~route (VCS.cur_tip ()) x
with e ->
let e = CErrors.push e in
Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)
end; `Ok
+ (* Part of the script commands don't set the query route *)
| VtQuery (true, _route), w ->
let id = VCS.new_node ~id:newtip () in
let queue =
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 73709268a4..33e5d532ad 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
p = q.
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
Set Default Proof Mode "Classic".
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 179f81e668..a664a1ef1d 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -3,7 +3,6 @@
(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
Set Default Proof Mode "Classic".
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y" (at level 70, no associativity).
@@ -14,7 +13,6 @@ Axiom admit : forall {T}, T.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Reserved Infix "o" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
Global Set Primitive Projections.
Delimit Scope morphism_scope with morphism.
Record PreCategory :=
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index edcd53005e..2b0fe13620 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -89,11 +89,5 @@ Open Scope type_scope.
(** ML Tactic Notations *)
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
-Declare ML Module "extratactics".
-Declare ML Module "g_auto".
-Declare ML Module "g_class".
-Declare ML Module "g_eqdecide".
-Declare ML Module "g_rewrite".
Global Set Default Proof Mode "Classic".
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 1e409607ae..886533586f 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -2,7 +2,7 @@ Require Import Notations.
Require Import Datatypes.
Require Import Logic.
-Local Declare ML Module "tauto".
+Declare ML Module "tauto_plugin".
Local Ltac not_dep_intros :=
repeat match goal with
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index c68c34bbbd..9224cdafe8 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -74,7 +74,9 @@ let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
{ require_modifiers None lexbuf }
- | "Local"? "Declare" space+ "ML" space+ "Module" space+
+ | "Local" space+ "Declare" space+ "ML" space+ "Module" space+
+ { modules [] lexbuf }
+ | "Declare" space+ "ML" space+ "Module" space+
{ modules [] lexbuf }
| "Load" space+
{ load_file lexbuf }
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 007b70bc0f..2e8ebb8531 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -417,7 +417,7 @@ let context poly l =
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
- let _ = Command.declare_definition id decl entry [] [] hook in
+ let _ = DeclareDef.declare_definition id decl entry [] [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 4064773561..fd49e53243 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -145,59 +145,6 @@ let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
-let warn_local_declaration =
- CWarnings.create ~name:"local-declaration" ~category:"scope"
- (fun (id,kind) ->
- pr_id id ++ strbrk " is declared as a local " ++ str kind)
-
-let get_locality id ~kind = function
-| Discharge ->
- (** If a Let is defined outside a section, then we consider it as a local definition *)
- warn_local_declaration (id,kind);
- true
-| Local -> true
-| Global -> false
-
-let declare_global_definition ident ce local k pl imps =
- let local = get_locality ident ~kind:"definition" local in
- let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
- let gr = ConstRef kn in
- let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
- let () = definition_message ident in
- gr
-
-let declare_definition_hook = ref ignore
-let set_declare_definition_hook = (:=) declare_definition_hook
-let get_declare_definition_hook () = !declare_definition_hook
-
-let warn_definition_not_visible =
- CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
- (fun ident ->
- strbrk "Section definition " ++
- pr_id ident ++ strbrk " is not visible from current goals")
-
-let declare_definition ident (local, p, k) ce pl imps hook =
- let fix_exn = Future.fix_exn_of ce.const_entry_body in
- let () = !declare_definition_hook ce in
- let r = match local with
- | Discharge when Lib.sections_are_opened () ->
- let c = SectionLocalDef ce in
- let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
- let () = definition_message ident in
- let gr = VarRef ident in
- let () = maybe_declare_manual_implicits false gr imps in
- let () = if Proof_global.there_are_pending_proofs () then
- warn_definition_not_visible ident
- in
- gr
- | Discharge | Local | Global ->
- declare_global_definition ident ce local k pl imps in
- Lemmas.call_hook fix_exn hook local r
-
-let _ = Obligations.declare_definition_ref :=
- (fun i k c imps hook -> declare_definition i k c [] imps hook)
-
let do_definition ident k pl bl red_option c ctypopt hook =
let (ce, evd, pl', imps as def) =
interp_definition pl bl (pi2 k) red_option c ctypopt
@@ -220,7 +167,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(declare_definition ident k ce pl' imps
+ ignore(DeclareDef.declare_definition ident k ce pl' imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
@@ -243,7 +190,7 @@ match local with
(r,Univ.Instance.empty,true)
| Global | Local | Discharge ->
- let local = get_locality ident ~kind:"axiom" local in
+ let local = DeclareDef.get_locality ident ~kind:"axiom" local in
let inl = match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
@@ -876,13 +823,6 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
- let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
- declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
-
-let _ = Obligations.declare_fix_ref :=
- (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
-
let prepare_recursive_declaration fixnames fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
let names = List.map (fun id -> Name id) fixnames in
@@ -1226,7 +1166,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let evd = Evd.restrict_universe_context evd vars in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let pl, ctx = Evd.universe_context ?names:pl evd in
- ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
@@ -1257,7 +1197,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
let pl, ctx = Evd.universe_context ?names:pl evd in
- ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
diff --git a/vernac/command.mli b/vernac/command.mli
index a636bc03c5..1887885de9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -23,11 +23,6 @@ val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
(Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
-(** {6 Hooks for Pcoq} *)
-
-val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
-
(** {6 Definitions/Let} *)
val interp_definition :
@@ -35,10 +30,6 @@ val interp_definition :
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
Universes.universe_binders * Impargs.manual_implicits
-val declare_definition : Id.t -> definition_kind ->
- Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
- Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-
val do_definition : Id.t -> definition_kind -> lident list option ->
local_binder_expr list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
@@ -170,6 +161,3 @@ val do_cofixpoint :
(** Utils *)
val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit
-
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
- Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
new file mode 100644
index 0000000000..d7a4fcca3d
--- /dev/null
+++ b/vernac/declareDef.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Decl_kinds
+open Declare
+open Entries
+open Globnames
+open Impargs
+open Nameops
+
+let warn_definition_not_visible =
+ CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
+ Pp.(fun ident ->
+ strbrk "Section definition " ++
+ pr_id ident ++ strbrk " is not visible from current goals")
+
+let warn_local_declaration =
+ CWarnings.create ~name:"local-declaration" ~category:"scope"
+ Pp.(fun (id,kind) ->
+ pr_id id ++ strbrk " is declared as a local " ++ str kind)
+
+let get_locality id ~kind = function
+| Discharge ->
+ (** If a Let is defined outside a section, then we consider it as a local definition *)
+ warn_local_declaration (id,kind);
+ true
+| Local -> true
+| Global -> false
+
+let declare_global_definition ident ce local k pl imps =
+ let local = get_locality ident ~kind:"definition" local in
+ let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+ let gr = ConstRef kn in
+ let () = maybe_declare_manual_implicits false gr imps in
+ let () = Universes.register_universe_binders gr pl in
+ let () = definition_message ident in
+ gr
+
+let declare_definition ident (local, p, k) ce pl imps hook =
+ let fix_exn = Future.fix_exn_of ce.const_entry_body in
+ let r = match local with
+ | Discharge when Lib.sections_are_opened () ->
+ let c = SectionLocalDef ce in
+ let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
+ let () = definition_message ident in
+ let gr = VarRef ident in
+ let () = maybe_declare_manual_implicits false gr imps in
+ let () = if Proof_global.there_are_pending_proofs () then
+ warn_definition_not_visible ident
+ in
+ gr
+ | Discharge | Local | Global ->
+ declare_global_definition ident ce local k pl imps in
+ Lemmas.call_hook fix_exn hook local r
+
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+ let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+ declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
new file mode 100644
index 0000000000..5dea0ba272
--- /dev/null
+++ b/vernac/declareDef.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Decl_kinds
+open Names
+
+val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
+
+val declare_definition : Id.t -> definition_kind ->
+ Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+ Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
+
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+ Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 135e4c63ab..c0acdaf57d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -22,9 +22,6 @@ open Util
module NamedDecl = Context.Named.Declaration
-let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
-let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
-
let get_fix_exn, stm_get_fix_exn = Hook.make ()
let succfix (depth, fixrels) =
@@ -496,14 +493,12 @@ let declare_definition prg =
in
let () = progmap_remove prg in
let cst =
- !declare_definition_ref prg.prg_name
- prg.prg_kind ce prg.prg_implicits
+ DeclareDef.declare_definition prg.prg_name
+ prg.prg_kind ce [] prg.prg_implicits
(Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
in
Universes.register_universe_binders cst pl;
cst
-
-open Pp
let rec lam_index n t acc =
match kind_of_term t with
@@ -569,7 +564,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let ctx = Evd.evar_context_universe_context first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a276f9f9a3..9cbbf6082c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,23 +12,12 @@ open Evd
open Names
open Pp
open Globnames
-open Decl_kinds
-
-(** Forward declaration. *)
-val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
- Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
-
-val declare_definition_ref :
- (Id.t -> definition_kind ->
- Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
- -> global_reference Lemmas.declaration_hook -> global_reference) ref
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
-
val check_evars : env -> evar_map -> unit
val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index d631fae8a8..f74073e1f7 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -8,6 +8,7 @@ Metasyntax
Auto_ind_decl
Search
Indschemes
+DeclareDef
Obligations
Command
Classes
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:29:21 +0000