diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-28 23:30:12 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-28 23:30:12 +0000 |
| commit | 8878a1974cf41ea40e411785d1197f2722a50445 (patch) | |
| tree | d0b61b5adf8290304ee8d90ea4b655550592bbf3 /proofs/decl_mode.ml | |
| parent | 4d5984258731e82c17535cbe9c257cf639374151 (diff) | |
"suffices" implemented + syntax cleanup
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/decl_mode.ml')
| -rw-r--r-- | proofs/decl_mode.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 2e54f3743..5428166a9 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -68,9 +68,9 @@ type stack_info = type pm_info = { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) + 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" |