diff options
| author | barras | 2006-10-16 17:11:44 +0000 |
|---|---|---|
| committer | barras | 2006-10-16 17:11:44 +0000 |
| commit | 744e7f6a319f4d459a3cc2309f575d43041d75aa (patch) | |
| tree | f130166bae5b1c1aa39860e8e5a2e79bfa284296 /proofs/proof_type.mli | |
| parent | 8fe195799d9bf4eb0c84fad3e9a79b78e6e224ec (diff) | |
affichage des ... dans les scripts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 74c36c9811..9c82239ef3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -72,7 +72,7 @@ type prim_rule = [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal and gave [l] as subproofs to be completed. - if [ref = (Some(Tactic (t,p),l))] then [p] is the proof + if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof that the goal can be proven if the goals in [l] are solved. *) type proof_tree = { open_subgoals : int; @@ -87,7 +87,8 @@ and rule = | Change_evars and compound_rule= - | Tactic of tactic_expr + (* the boolean of Tactic tells if the default tactic is used *) + | Tactic of tactic_expr * bool | Proof_instr of bool * proof_instr and goal = evar_info |