Imported Upstream version 8.5~beta1+dfsg

1 files changed, 110 insertions, 44 deletions

diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 08ae7519..2700e901 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,14 +28,13 @@ type proof_mode = {
     It corresponds to Coq default setting are they are set when coqtop starts. *)
 val register_proof_mode : proof_mode -> unit
 
-val there_is_a_proof : unit -> bool
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
-val get_current_proof_name : unit -> Names.identifier
-val get_all_proof_names : unit -> Names.identifier list
+val get_current_proof_name : unit -> Names.Id.t
+val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Names.identifier Util.located -> unit
+val discard : Names.Id.t Loc.located -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -45,53 +44,102 @@ val set_proof_mode : string -> unit
 
 exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
+(** @raise NoCurrentProof when outside proof mode. *)
 
+val compact_the_proof : unit -> unit
 
-(** [start_proof s str goals ~init_tac ~compute_guard hook] starts 
-    a proof of name [s] and
-    conclusion [t]; [hook] is optionally a function to be applied at
-    proof end (e.g. to declare the built constructions as a coercion
-    or a setoid morphism). *)
+(** When a proof is closed, it is reified into a [proof_object], where
+    [id] is the name of the proof, [entries] the list of the proof terms
+    (in a form suitable for definitions). Together with the [terminator]
+    function which takes a [proof_object] together with a [proof_end]
+    (i.e. an proof ending command) and registers the appropriate
+    values. *)
 type lemma_possible_guards = int list list
-val start_proof : Names.identifier -> 
-                          Decl_kinds.goal_kind ->
-                          (Environ.env * Term.types) list  ->
-                          ?compute_guard:lemma_possible_guards -> 
-                          Tacexpr.declaration_hook -> 
-                          unit
-
-val close_proof : unit -> 
-                           Names.identifier * 
-                          (Entries.definition_entry list * 
-			    lemma_possible_guards * 
-			    Decl_kinds.goal_kind * 
-			    Tacexpr.declaration_hook)
+type proof_universes = Evd.evar_universe_context
+type proof_object = {
+  id : Names.Id.t;
+  entries : Entries.definition_entry list;
+  persistence : Decl_kinds.goal_kind;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
+  (** guards : lemma_possible_guards; *)
+}
+
+type proof_ending =
+  | Admitted
+  | Proved of Vernacexpr.opacity_flag *
+             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              proof_object
+type proof_terminator = proof_ending -> unit
+type closed_proof = proof_object * proof_terminator
+
+(** [start_proof id str goals terminator] starts a proof of name [id]
+    with goals [goals] (a list of pairs of environment and
+    conclusion); [str] describes what kind of theorem/definition this
+    is (spiwack: for potential printing, I believe is used only by
+    closing commands and the xml plugin); [terminator] is used at the
+    end of the proof to close the proof. *)
+val start_proof :
+  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+    proof_terminator -> unit
+
+(** Like [start_proof] except that there may be dependencies between
+    initial goals. *)
+val start_dependent_proof :
+  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
+    proof_terminator -> unit
+
+(* Takes a function to add to the exceptions data relative to the
+   state in which the proof was built *)
+val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
+
+(* Intermediate step necessary to delegate the future.
+ * Both access the current proof state. The formes is supposed to be
+ * chained with a computation that completed the proof *)
+
+type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+
+val return_proof : unit -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t ->
+  closed_proof_output Future.computation -> closed_proof
+
+(** Gets the current terminator without checking that the proof has
+    been completed. Useful for the likes of [Admitted]. *)
+val get_terminator : unit -> proof_terminator
+val set_terminator : proof_terminator -> unit
 
 exception NoSuchProof
 
-(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
-   no current proof. *)
-val run_tactic : unit Proofview.tactic -> unit
+val get_open_goals : unit -> int
 
-(** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : unit Proofview.tactic -> unit
+(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
+    no current proof.
+    The return boolean is set to [false] if an unsafe tactic has been used. *)
+val with_current_proof :
+  (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
+val simple_with_current_proof :
+  (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
-(** Sets the section variables assumed by the proof *)
-val set_used_variables : Names.identifier list -> unit
-val get_used_variables : unit -> Sign.section_context option
+(** Sets the tactic to be used when a tactic line is closed with [...] *)
+val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
+val set_interp_tac :
+  (Tacexpr.raw_tactic_expr -> unit Proofview.tactic)
+    -> unit
 
-(** Appends the endline tactic of the current proof to a tactic. *)
-val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
+(** Sets the section variables assumed by the proof, returns its closure
+ * (w.r.t. type dependencies *)
+val set_used_variables : Names.Id.t list -> Context.section_context
+val get_used_variables : unit -> Context.section_context option
 
 (**********************************************************)
-(*                                                                                                  *)
-(*                              Utility functions                                          *)
-(*                                                                                                  *)
+(*                                                        *)
+(*                            Proof modes                 *)
+(*                                                        *)
 (**********************************************************)
 
-(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a
-    focused goal or that the last focus isn't of kind [k]. *)
-val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
+
+val activate_proof_mode : string -> unit
+val disactivate_proof_mode : string -> unit
 
 (**********************************************************)
 (*                                                        *)
@@ -103,11 +151,13 @@ module Bullet : sig
   type t = Vernacexpr.bullet
 
   (** A [behavior] is the data of a put function which
-      is called when a bullet prefixes a tactic, together
-      with a name to identify it. *)
+      is called when a bullet prefixes a tactic, a suggest function
+      suggesting the right bullet to use on a given proof, together
+      with a name to identify the behavior. *)
   type behavior = {
     name : string;
-    put : Proof.proof -> t -> unit
+    put : Proof.proof -> t -> Proof.proof;
+    suggest: Proof.proof -> string option
   }
 
   (** A registered behavior can then be accessed in Coq
@@ -123,9 +173,25 @@ module Bullet : sig
 
   (** Handles focusing/defocusing with bullets:
        *)
-  val put : Proof.proof -> t -> unit
+  val put : Proof.proof -> t -> Proof.proof
+  val suggest : Proof.proof -> string option
 end
 
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
+  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+  Decl_kinds.goal_kind)
 end
+
+type state
+val freeze : marshallable:[`Yes | `No | `Shallow] -> state
+val unfreeze : state -> unit
+val proof_of_state : state -> Proof.proof