aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v8
-rw-r--r--doc/refman/RefMan-tac.tex9
-rw-r--r--ide/wg_ProofView.ml22
-rw-r--r--lib/interface.mli2
-rw-r--r--lib/serialize.ml8
-rw-r--r--printing/printer.ml17
-rw-r--r--proofs/proof.ml17
-rw-r--r--proofs/proof.mli8
-rw-r--r--proofs/proof_global.ml5
-rw-r--r--proofs/proofview.ml18
-rw-r--r--proofs/proofview.mli9
-rw-r--r--proofs/proofview_gen.ml603
-rw-r--r--proofs/proofview_monad.mli4
-rw-r--r--tactics/extratactics.ml48
-rw-r--r--toplevel/ide_slave.ml8
15 files changed, 432 insertions, 314 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 581fafad8..a6b7bad12 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -569,10 +569,12 @@ Record proofview := {
}.
Definition LogicalState := proofview.
-(** Logical Message: status (safe/unsafe) * shelved goals *)
-Definition LogicalMessageType := (bool * list goal)%type.
+(** Logical Message: status (safe/unsafe) * ( shelved goals * given up ) *)
+Definition LogicalMessageType := ( bool * ( list goal * list goal ))%type.
Definition LogicalEnvironment := env.
-Definition LogicalMessage : Monoid.T LogicalMessageType := Monoid.cart Monoid.BoolAnd Monoid.List.
+Definition LogicalMessage : Monoid.T LogicalMessageType :=
+ Monoid.cart Monoid.BoolAnd (Monoid.cart Monoid.List Monoid.List)
+.
Definition NonLogicalType := IO.T.
Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a78e3448e..88a16e014 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4626,7 +4626,7 @@ back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
Shelves only these goals under focused which are mentioned in other goals.
Goals which appear in the type of other goals can be solve by unification.
-
+
\Example
\begin{coq_example}
Goal exists n, n=0.
@@ -4646,6 +4646,13 @@ Reset Initial.
This command moves all the goals on the shelf (see Section~\ref{shelve}) from the
shelf into focus, by appending them to the end of the current list of focused goals.
+\subsection[\tt give\_up]{\tt give\_up\tacindex{give\_up}}
+
+This tactic removes the focused goals from the proof. They are not solved, and cannot
+be solved later in the proof. As the goals are not solved, the proof cannot be closed.
+
+The {\tt give\_up} tactic can be used while editing a proof, to choose to write the
+proof script in a non-sequential order.
\section{Simple tactic macros}
\index{Tactic macros}
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 1a333ff16..8c7aeeb8c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -129,13 +129,13 @@ let display mode (view : #GText.view_skel) goals hints evars =
match goals with
| None -> ()
(* No proof in progress *)
- | Some { Interface.fg_goals = []; Interface.bg_goals = bg; shelved_goals = shelf } ->
+ | Some { Interface.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } ->
let bg = flatten (List.rev bg) in
let evars = match evars with None -> [] | Some evs -> evs in
- begin match (bg, shelf, evars) with
- | [], [], [] ->
+ begin match (bg, shelved_goals,given_up_goals, evars) with
+ | [], [], [], [] ->
view#buffer#insert "No more subgoals."
- | [], [], _ :: _ ->
+ | [], [], [], _ :: _ ->
(* A proof has been finished, but not concluded *)
view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
let iter evar =
@@ -143,15 +143,23 @@ let display mode (view : #GText.view_skel) goals hints evars =
view#buffer#insert msg
in
List.iter iter evars
- | [], _, _ ->
+ | [], [], _, _ ->
+ (* The proof is finished, with the exception of given up goals. *)
+ view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n";
+ let iter goal =
+ let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+ view#buffer#insert msg
+ in
+ List.iter iter given_up_goals
+ | [], _, _, _ ->
(* All the goals have been resolved but those on the shelf. *)
view#buffer#insert "All the remaining goals are on the shelf:\n\n";
let iter goal =
let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
view#buffer#insert msg
in
- List.iter iter shelf
- | _, _, _ ->
+ List.iter iter shelved_goals
+ | _, _, _, _ ->
(* No foreground proofs, but still unfocused ones *)
view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
let iter goal =
diff --git a/lib/interface.mli b/lib/interface.mli
index d19027256..31577e629 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -46,6 +46,8 @@ type goals = {
(** Zipper representing the unfocussed background goals *)
shelved_goals : goal list;
(** List of the goals on the shelf. *)
+ given_up_goals : goal list;
+ (** List of the goals that have been given up *)
}
type hint = (string * string) list
diff --git a/lib/serialize.ml b/lib/serialize.ml
index f3c06d930..743247faf 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -259,14 +259,16 @@ let of_goals g =
let fg = of_list of_goal g.fg_goals in
let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
let shelf = of_list of_goal g.shelved_goals in
- Element ("goals", [], [fg; bg; shelf])
+ let given_up = of_list of_goal g.given_up_goals in
+ Element ("goals", [], [fg; bg; shelf; given_up])
let to_goals = function
- | Element ("goals", [], [fg; bg; shelf]) ->
+ | Element ("goals", [], [fg; bg; shelf; given_up]) ->
let to_glist = to_list to_goal in
let fg = to_list to_goal fg in
let bg = to_list (to_pair to_glist to_glist) bg in
let shelf = to_list to_goal shelf in
- { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; }
+ let given_up = to_list to_goal given_up in
+ { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up }
| _ -> raise Marshal_error
let of_coq_info info =
diff --git a/printing/printer.ml b/printing/printer.ml
index d91829420..496f9b87e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -540,21 +540,28 @@ let pr_open_subgoals () =
straightforward, but seriously, [Proof.proof] should return
[evar_info]-s instead. *)
let p = Proof_global.give_me_the_proof () in
- let (goals , stack , shelf, sigma ) = Proof.proof p in
+ let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in
let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
let seeds = Proof.V82.top_evars p in
begin match goals with
| [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
- begin match bgoals,shelf with
- | [],[] -> pr_subgoals None sigma seeds shelf stack goals
- | [] , _ ->
+ begin match bgoals,shelf,given_up with
+ | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+ | [] , [] , _ ->
+ (* emacs mode: xml-like flag for detecting information message *)
+ str (emacs_str "<infomsg>") ++
+ str "No more, however there are goals you gave up. You need to go back and solve them."
+ ++ str (emacs_str "</infomsg>")
+ ++ fnl () ++ fnl ()
+ ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+ | [] , _ , _ ->
(* emacs mode: xml-like flag for detecting information message *)
str (emacs_str "<infomsg>") ++
str "All the remaining goals are on the shelf."
++ str (emacs_str "</infomsg>")
++ fnl () ++ fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
- | _ , _ ->
+ | _ , _, _ ->
(* emacs mode: xml-like flag for detecting information message *)
str (emacs_str "<infomsg>") ++
str "This subproof is complete, but there are still unfocused goals."
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 6b847ec01..99654ab75 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -93,6 +93,8 @@ type proof = {
focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
(* List of goals that have been shelved. *)
shelf : Goal.goal list;
+ (* List of goals that have been given up *)
+ given_up : Goal.goal list;
}
(*** General proof functions ***)
@@ -110,7 +112,8 @@ let proof p =
map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
in
let shelf = p.shelf in
- (goals,stack,shelf,sigma)
+ let given_up = p.given_up in
+ (goals,stack,shelf,given_up,sigma)
let rec unroll_focus pv = function
| (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
@@ -227,15 +230,18 @@ let start goals =
let pr = {
proofview = Proofview.init goals ;
focus_stack = [] ;
- shelf = [] } in
+ shelf = [] ;
+ given_up = [] } in
_focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
exception UnfinishedProof
exception HasShelvedGoals
+exception HasGivenUpGoals
exception HasUnresolvedEvar
let _ = Errors.register_handler begin function
| UnfinishedProof -> Errors.error "Some goals have not been solved."
| HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
+ | HasGivenUpGoals -> Errors.error "Some goals have been given up."
| HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
| _ -> raise Errors.Unhandled
end
@@ -245,6 +251,8 @@ let return p =
raise UnfinishedProof
else if not (CList.is_empty (p.shelf)) then
raise HasShelvedGoals
+ else if not (CList.is_empty (p.given_up)) then
+ raise HasGivenUpGoals
else if has_unresolved_evar p then
(* spiwack: for compatibility with <= 8.3 proof engine *)
raise HasUnresolvedEvar
@@ -260,7 +268,7 @@ let initial_goals p = Proofview.initial_goals p.proofview
let run_tactic env tac pr =
let sp = pr.proofview in
- let (_,tacticced_proofview,(status,to_shelve)) = Proofview.apply env tac sp in
+ let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in
let shelf =
let pre_shelf = pr.shelf@to_shelve in
(* Compacting immediately: if someone shelves a goal, he probably
@@ -271,7 +279,8 @@ let run_tactic env tac pr =
end
end
in
- { pr with proofview = tacticced_proofview ; shelf },status
+ let given_up = pr.given_up@give_up in
+ { pr with proofview = tacticced_proofview ; shelf ; given_up },status
let emit_side_effects eff pr =
{pr with proofview = Proofview.emit_side_effects eff pr.proofview}
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 0df55759d..4f7a242d3 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -40,13 +40,15 @@ type proof
functions to ide-s. This would be better than spawning a new nearly
identical function everytime. Hence the generic name. *)
(* In this version: returns the focused goals, a representation of the
- focus stack (the goals at each level), a representation
- of the shelf (the list of goals on the shelf),and the underlying
+ focus stack (the goals at each level), a representation of the
+ shelf (the list of goals on the shelf), a representation of the
+ given up goals (the list of the given up goals) and the underlying
evar_map *)
val proof : proof ->
Goal.goal list
* (Goal.goal list * Goal.goal list) list
* Goal.goal list
+ * Goal.goal list
* Evd.evar_map
(*** General proof functions ***)
@@ -64,9 +66,11 @@ val partial_proof : proof -> Term.constr list
(* Returns the proofs (with their type) of the initial goals.
Raises [UnfinishedProof] is some goals remain to be considered.
Raises [HasShelvedGoals] if some goals are left on the shelf.
+ Raises [HasGivenUpGoals] if some goals have been given up.
Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
exception UnfinishedProof
exception HasShelvedGoals
+exception HasGivenUpGoals
exception HasUnresolvedEvar
val return : proof -> Evd.evar_map
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3c0e29023..ac61f4e67 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -262,7 +262,7 @@ let set_used_variables l =
pstates := { p with section_vars = Some ctx} :: rest
let get_open_goals () =
- let gl, gll, shelf , _ = Proof.proof (cur_pstate ()).proof in
+ let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
List.length gl +
List.fold_left (+) 0
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
@@ -297,6 +297,9 @@ let return_proof () =
| Proof.HasShelvedGoals ->
raise (Errors.UserError("last tactic before Qed",
str"Attempt to save a proof with shelved goals"))
+ | Proof.HasGivenUpGoals ->
+ raise (Errors.UserError("last tactic before Qed",
+ str"Attempt to save a proof with given up goals"))
| Proof.HasUnresolvedEvar ->
raise (Errors.UserError("last tactic before Qed",
str"Attempt to save a proof with existential " ++
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f08689538..dd05184c4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -565,7 +565,7 @@ let tclTIMEOUT n t =
| Util.Inr e -> tclZERO e
let mark_as_unsafe =
- Proof.put (false,[])
+ Proof.put (false,([],[]))
(* Shelves all the goals under focus. *)
let shelve =
@@ -574,7 +574,7 @@ let shelve =
let (>>) = Proof.seq in
Proof.get >>= fun initial ->
Proof.set {initial with comb=[]} >>
- Proof.put (true,initial.comb)
+ Proof.put (true,(initial.comb,[]))
(* Shelves the unifiable goals under focus, i.e. the goals which
appear in other goals under focus (the unfocused goals are not
@@ -586,13 +586,23 @@ let shelve_unifiable =
Proof.get >>= fun initial ->
let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
Proof.set {initial with comb=n} >>
- Proof.put (true,u)
+ Proof.put (true,(u,[]))
(* [unshelve l p] adds all the goals in [l] at the end of the focused
goals of p *)
let unshelve l p =
{ p with comb = p.comb@l }
+(* Gives up on the goal under focus. Reports an unsafe status. Proofs
+ with given up goals cannot be closed. *)
+let give_up =
+ (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+ let (>>=) = Proof.bind in
+ let (>>) = Proof.seq in
+ Proof.get >>= fun initial ->
+ Proof.set {initial with comb=[]} >>
+ Proof.put (false,([],initial.comb))
+
(*** Commands ***)
let in_proofview p k =
@@ -716,7 +726,7 @@ module V82 = struct
with Proof_errors.TacticFailure e -> raise e
let put_status b =
- Proof.put (b,[])
+ Proof.put (b,([],[]))
let catchable_exception = catchable_exception
end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0899f52dd..635f2fd47 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -120,7 +120,9 @@ type +'a tactic
(* Applies a tactic to the current proofview. *)
(* the return boolean signals the use of an unsafe tactic, in which
case it is [false]. *)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * (bool*Goal.goal list)
+val apply : Environ.env -> 'a tactic -> proofview -> 'a
+ * proofview
+ * (bool*(Goal.goal list*Goal.goal list))
(*** tacticals ***)
@@ -223,6 +225,11 @@ val shelve_unifiable : unit tactic
goals of p *)
val unshelve : Goal.goal list -> proofview -> proofview
+
+(* Gives up on the goal under focus. Reports an unsafe status. Proofs
+ with given up goals cannot be closed. *)
+val give_up : unit tactic
+
exception Timeout
(** [tclTIMEOUT n t] can have only one success.
In case of timeout if fails with [tclZERO Timeout]. *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index b813eabaa..18f834910 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -101,7 +101,8 @@ type proofview = { initial : (Term.constr*Term.types)
type logicalState = proofview
-type logicalMessageType = bool*Goal.goal list
+type logicalMessageType =
+ bool*(Goal.goal list*Goal.goal list)
type logicalEnvironment = Environ.env
@@ -187,68 +188,73 @@ module Logical =
struct
type 'a t =
__ -> ('a -> proofview -> __ -> (__ -> __
- -> (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T) -> __ -> (__ -> (exn
- -> __ IOBase.coq_T) -> __ IOBase.coq_T)
- -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> Environ.env -> __ -> (__
- -> (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T) -> __ -> (__ -> (exn
+ -> (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-> __ IOBase.coq_T) -> __ IOBase.coq_T)
- -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> proofview -> __ -> (__
- -> __ -> (__ -> (bool*Goal.goal list) ->
+ -> __ -> (__ -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list)) ->
__ -> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T) -> Environ.env -> __
- -> (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
+ -> __ IOBase.coq_T) -> proofview -> __ ->
+ (__ -> __ -> (__ -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
-> __ IOBase.coq_T) -> __ -> (__ -> (exn
-> __ IOBase.coq_T) -> __ IOBase.coq_T)
-> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T
+ IOBase.coq_T) -> Environ.env -> __ -> (__
+ -> (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __
+ -> (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
+ -> __ IOBase.coq_T
(** val ret :
'a1 -> __ -> ('a1 -> proofview -> __ ->
- ('a2 -> __ -> (__ -> (bool*Goal.goal
- list) -> __ -> (__ -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) ->
+ ('a2 -> __ -> (__ -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> __ -> (__ -> (exn ->
- __ IOBase.coq_T) -> __ IOBase.coq_T) ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> Environ.env -> __ ->
- (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ Environ.env -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let ret x =
(); (fun _ k s -> Obj.magic k x s)
@@ -256,37 +262,39 @@ module Logical =
(** val bind :
'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
-> proofview -> __ -> ('a3 -> __ -> (__
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a3 -> __ -> ('a4
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a3 -> __ -> ('a4 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a4 ->
- (bool*Goal.goal list) -> __ -> ('a5 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a5 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a5 -> (exn -> 'a6 IOBase.coq_T) ->
- 'a6 IOBase.coq_T) -> (exn -> 'a6
- IOBase.coq_T) -> 'a6 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a5 -> (exn ->
+ 'a6 IOBase.coq_T) -> 'a6 IOBase.coq_T)
+ -> (exn -> 'a6 IOBase.coq_T) -> 'a6
+ IOBase.coq_T **)
let bind x k =
(); (fun _ k0 s ->
@@ -295,37 +303,40 @@ module Logical =
(** val ignore :
'a1 t -> __ -> (unit -> proofview -> __
- -> ('a2 -> __ -> (__ -> (bool*Goal.goal
- list) -> __ -> (__ -> (exn -> __
+ -> ('a2 -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> __ -> (__ -> (exn ->
__ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> Environ.env -> __ ->
- (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let ignore x =
(); (fun _ k s ->
@@ -334,37 +345,39 @@ module Logical =
(** val seq :
unit t -> 'a1 t -> __ -> ('a1 ->
proofview -> __ -> ('a2 -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let seq x k =
(); (fun _ k0 s ->
@@ -374,74 +387,79 @@ module Logical =
(** val set :
logicalState -> __ -> (unit ->
proofview -> __ -> ('a1 -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a1 -> __ -> ('a2
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a2 ->
- (bool*Goal.goal list) -> __ -> ('a3 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a3 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
- 'a4 IOBase.coq_T) -> (exn -> 'a4
- IOBase.coq_T) -> 'a4 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T **)
let set s =
(); (fun _ k x -> Obj.magic k () s)
(** val get :
__ -> (logicalState -> proofview -> __
- -> ('a1 -> __ -> (__ -> (bool*Goal.goal
- list) -> __ -> (__ -> (exn -> __
+ -> ('a1 -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> __ -> (__ -> (exn ->
__ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> Environ.env -> __ ->
- (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a1 -> __ -> ('a2
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a2 ->
- (bool*Goal.goal list) -> __ -> ('a3 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a3 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
- 'a4 IOBase.coq_T) -> (exn -> 'a4
- IOBase.coq_T) -> 'a4 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T **)
let get r k s =
Obj.magic k s s
@@ -449,117 +467,127 @@ module Logical =
(** val put :
logicalMessageType -> __ -> (unit ->
proofview -> __ -> ('a1 -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a1 -> __ -> ('a2
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a2 ->
- (bool*Goal.goal list) -> __ -> ('a3 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a3 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
- 'a4 IOBase.coq_T) -> (exn -> 'a4
- IOBase.coq_T) -> 'a4 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T **)
let put m =
(); (fun _ k s _ k0 e _ k1 ->
Obj.magic k () s __ k0 e __
(fun b c' ->
k1 b
- ((if fst m then fst c' else false),
- (List.append (snd m) (snd c')))))
+ ((if fst m then fst c' else false),(
+ (List.append (fst (snd m))
+ (fst (snd c'))),(List.append
+ (snd (snd m))
+ (snd (snd c')))))))
(** val current :
__ -> (logicalEnvironment -> proofview
-> __ -> ('a1 -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a1 -> __ -> ('a2
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a2 ->
- (bool*Goal.goal list) -> __ -> ('a3 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a3 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
- 'a4 IOBase.coq_T) -> (exn -> 'a4
- IOBase.coq_T) -> 'a4 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a3 -> (exn ->
+ 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
+ -> (exn -> 'a4 IOBase.coq_T) -> 'a4
+ IOBase.coq_T **)
let current r k s r0 k0 e =
Obj.magic k e s __ k0 e
(** val zero :
exn -> __ -> ('a1 -> proofview -> __ ->
- ('a2 -> __ -> (__ -> (bool*Goal.goal
- list) -> __ -> (__ -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) ->
+ ('a2 -> __ -> (__ -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> __ -> (__ -> (exn ->
- __ IOBase.coq_T) -> __ IOBase.coq_T) ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> Environ.env -> __ ->
- (__ -> (bool*Goal.goal list) -> __ ->
- (__ -> (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ Environ.env -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let zero e =
(); (fun _ k s _ k0 e0 _ k1 _ sk fk ->
@@ -568,37 +596,39 @@ module Logical =
(** val plus :
'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
-> proofview -> __ -> ('a2 -> __ -> (__
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let plus x y =
(); (fun _ k s _ k0 e _ k1 _ sk fk ->
@@ -610,44 +640,47 @@ module Logical =
(** val split :
'a1 t -> __ -> (('a1, exn -> 'a1 t)
list_view -> proofview -> __ -> ('a2 ->
- __ -> (__ -> (bool*Goal.goal list) ->
- __ -> (__ -> (exn -> __ IOBase.coq_T)
- -> __ IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
+ __ -> (__ -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ Environ.env -> __ -> (__ ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let split x =
(); (fun _ k s _ k0 e _ k1 _ sk fk ->
IOBase.bind
(Obj.magic x __ (fun a s' _ k2 e0 ->
k2 (a,s')) s __ (fun a _ k2 ->
- k2 a (true,[])) e __
+ k2 a (true,([],[]))) e __
(fun a c _ sk0 fk0 ->
sk0 (a,c) fk0) __ (fun a fk0 ->
IOBase.ret (Cons (a,
@@ -662,16 +695,17 @@ module Logical =
(fun x0 ->
match x0 with
| Nil exc ->
- let c = true,[] in
+ let c = true,([],[]) in
Obj.magic k (Nil exc) s __ k0 e __
(fun b c' ->
k1 b
((if fst c
then fst c'
- else false),(List.append
- (snd c)
- (snd c')))) __
- sk fk
+ else false),((List.append
+ (fst (snd c))
+ (fst (snd c'))),
+ (List.append (snd (snd c))
+ (snd (snd c')))))) __ sk fk
| Cons (p, y) ->
let p0,m' = p in
let a',s' = p0 in
@@ -685,53 +719,60 @@ module Logical =
k4 b
((if fst c
then fst c'
- else false),(List.append
- (snd c)
- (snd c'))))
- __ sk0 fk1) fk0))) s' __ k0 e
- __ (fun b c' ->
+ else false),((List.append
+ (fst
+ (snd c))
+ (fst
+ (snd c'))),
+ (List.append (snd (snd c))
+ (snd (snd c')))))) __ sk0
+ fk1) fk0))) s' __ k0 e __
+ (fun b c' ->
k1 b
((if fst m'
then fst c'
- else false),(List.append
- (snd m')
- (snd c')))) __
- sk fk))
+ else false),((List.append
+ (fst (snd m'))
+ (fst (snd c'))),
+ (List.append (snd (snd m'))
+ (snd (snd c')))))) __ sk fk))
(** val lift :
'a1 NonLogical.t -> __ -> ('a1 ->
proofview -> __ -> ('a2 -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
- (exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- Environ.env -> __ -> (__ ->
- (bool*Goal.goal list) -> __ -> (__ ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> (__ -> (exn -> __ IOBase.coq_T) ->
- __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> Environ.env -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal
+ list)) -> __ -> (__ -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
- proofview -> __ -> ('a2 -> __ -> ('a3
- -> (bool*Goal.goal list) -> __ -> (__
- -> (exn -> __ IOBase.coq_T) -> __
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ ->
+ ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+ list*Goal.goal list)) -> __ -> (__ ->
+ (exn -> __ IOBase.coq_T) -> __
IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) -> __
-> (__ -> (exn -> __ IOBase.coq_T) ->
__ IOBase.coq_T) -> (exn -> __
IOBase.coq_T) -> __ IOBase.coq_T) ->
Environ.env -> __ -> ('a3 ->
- (bool*Goal.goal list) -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list))
+ -> __ -> ('a4 -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) ->
(exn -> __ IOBase.coq_T) -> __
- IOBase.coq_T) -> (exn -> __
- IOBase.coq_T) -> __ IOBase.coq_T) -> __
- -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
- 'a5 IOBase.coq_T) -> (exn -> 'a5
- IOBase.coq_T) -> 'a5 IOBase.coq_T **)
+ IOBase.coq_T) -> __ -> ('a4 -> (exn ->
+ 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
+ -> (exn -> 'a5 IOBase.coq_T) -> 'a5
+ IOBase.coq_T **)
let lift x =
(); (fun _ k s _ k0 e _ k1 _ sk fk ->
@@ -739,12 +780,16 @@ module Logical =
Obj.magic k x0 s __ k0 e __
(fun b c' ->
k1 b
- ((if fst (true,[])
+ ((if fst (true,([],[]))
then fst c'
- else false),(List.append
- (snd (true,[]))
- (snd c')))) __ sk
- fk))
+ else false),((List.append
+ (fst
+ (snd
+ (true,([],[]))))
+ (fst (snd c'))),
+ (List.append
+ (snd (snd (true,([],[]))))
+ (snd (snd c')))))) __ sk fk))
(** val run :
'a1 t -> logicalEnvironment ->
@@ -755,9 +800,9 @@ module Logical =
let run x e s =
Obj.magic x __ (fun a s' _ k e0 ->
k (a,s')) s __ (fun a _ k ->
- k a (true,[])) e __ (fun a c _ sk fk ->
- sk (a,c) fk) __ (fun a x0 ->
- IOBase.ret a) (fun e0 ->
+ k a (true,([],[]))) e __
+ (fun a c _ sk fk -> sk (a,c) fk) __
+ (fun a x0 -> IOBase.ret a) (fun e0 ->
IOBase.raise
((fun e -> Proof_errors.TacticFailure e)
e0))
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index c1f1b5ee1..fa4392368 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -12,8 +12,8 @@ type logicalState = proofview
type logicalEnvironment = Environ.env
-(** status (safe/unsafe) * shelved goals *)
-type logicalMessageType = bool * Goal.goal list
+(** status (safe/unsafe) * ( shelved goals * given up ) *)
+type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a7a89eae7..e45c2170a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -824,3 +824,11 @@ VERNAC COMMAND EXTEND Unshelve
=> [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
-> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ]
END
+
+(* Gives up on the goals under focus: the goals are considered solved,
+ but the proof cannot be closed until the user goes back and solve
+ these goals. *)
+TACTIC EXTEND give_up
+| [ "give_up" ] ->
+ [ Proofview.give_up ]
+END
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 48afe324e..a519b5881 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -193,7 +193,7 @@ let goals () =
if not (String.is_empty s) then msg_info (str s);
try
let pfts = Proof_global.give_me_the_proof () in
- let (goals, zipper, shelf, sigma) = Proof.proof pfts in
+ let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in
let fg = List.map (process_goal sigma) goals in
let map_zip (lg, rg) =
let lg = List.map (process_goal sigma) lg in
@@ -202,7 +202,11 @@ let goals () =
in
let bg = List.map map_zip zipper in
let shelf = List.map (process_goal sigma) shelf in
- Some { Interface.fg_goals = fg; Interface.bg_goals = bg; shelved_goals = shelf; }
+ let given_up = List.map (process_goal sigma) given_up in
+ Some { Interface.fg_goals = fg;
+ Interface.bg_goals = bg;
+ shelved_goals = shelf;
+ given_up_goals = given_up; }
with Proof_global.NoCurrentProof -> None
let evars () =
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 01:05:07 +0000