diff options
Diffstat (limited to 'toplevel/backtrack.ml')
| -rw-r--r-- | toplevel/backtrack.ml | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 24a056d7..912d694e 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,12 +33,18 @@ type info = { nproofs : int; prfname : identifier option; prfdepth : int; + ngoals : int; cmd : vernac_expr; mutable reachable : bool; } let history : info Stack.t = Stack.create () +(** Is this stack active (i.e. nonempty) ? + The stack is currently inactive when compiling files (coqc). *) + +let is_active () = not (Stack.is_empty history) + (** For debug purpose, a dump of the history *) let dump_history () = @@ -74,6 +80,14 @@ let search test = with Found i -> while i != Stack.top history do pop () done +(** An auxiliary function to retrieve the number of remaining subgoals *) + +let get_ngoals () = + try + let prf = Proof_global.give_me_the_proof () in + List.length (Evd.sig_it (Proof.V82.background_subgoals prf)) + with Proof_global.NoCurrentProof -> 0 + (** Register the end of a command and store the current state *) let mark_command ast = @@ -85,6 +99,7 @@ let mark_command ast = prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); prfdepth = max 0 (Pfedit.current_proof_depth ()); reachable = true; + ngoals = get_ngoals (); cmd = ast } history @@ -175,6 +190,7 @@ let reset_initial () = nproofs = 0; prfname = None; prfdepth = 0; + ngoals = 0; reachable = true; cmd = VernacNop } history @@ -215,10 +231,10 @@ let get_script prf = | _ -> () in (try Stack.iter select history with Not_found -> ()); - (* Get rid of intermediate commands which don't grow the depth *) + (* Get rid of intermediate commands which don't grow the proof depth *) let rec filter n = function | [] -> [] - | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l + | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l | {prfdepth=d}::l -> filter d l in (* initial proof depth (after entering the lemma statement) is 1 *) |