diff options
| author | corbinea | 2007-04-26 08:54:28 +0000 |
|---|---|---|
| committer | corbinea | 2007-04-26 08:54:28 +0000 |
| commit | ea1eaa9b152b73652f417e02bd469e5b289cec47 (patch) | |
| tree | 4d654ad1434bac0781eb4f3e6f1505c3895df4ba /proofs | |
| parent | 40425048feff138e6c67555c7ee94142452d1cae (diff) | |
fin des conclusions multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/decl_expr.mli | 1 | ||||
| -rw-r--r-- | proofs/decl_mode.ml | 10 | ||||
| -rw-r--r-- | proofs/decl_mode.mli | 7 |
3 files changed, 9 insertions, 9 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index 1c5cc0e746..d02060fc0a 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -18,7 +18,6 @@ type 'it statement = type thesis_kind = Plain - | Sub of int | For of identifier type 'this or_thesis = diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 5428166a99..cb148f4e54 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -67,10 +67,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list} + { pm_stack : stack_info list} let pm_in,pm_out = Dyn.create "pm_info" @@ -118,3 +115,8 @@ let get_end_command pts = end | Mode_none -> error "no proof in progress" + +let get_last env = + try + let (id,_,_) = List.hd (Environ.named_context env) in id + with Invalid_argument _ -> error "no previous statement to use" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 4a8aa85f12..412624b4db 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -56,10 +56,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + {pm_stack : stack_info list } val pm_in : pm_info -> Dyn.t @@ -70,3 +67,5 @@ val get_end_command : pftreestate -> string option val get_stack : pftreestate -> stack_info list val get_top_stack : pftreestate -> stack_info list + +val get_last: Environ.env -> identifier |