diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-20 14:07:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-20 14:07:14 +0000 |
| commit | 8a6e3f648fa3171e3583e7c93c8967ac853a0d60 (patch) | |
| tree | 835f86f9c226e91b3f0be73342faa08fd1d4d755 /tactics | |
| parent | 18d4283e4129f6f347970c76d209817f1f66f232 (diff) | |
- Fixing declarative mode in presence of high use of Change_evars nodes
(bug 2092 and decl_mode.v in test suite).
- Added a debugging printer for pftreestate.
- Fixing American spelling in RefMan-decl.tex.
- Optimizing application of tactic validation by removing consistency
test in descend.
- Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 10 |
2 files changed, 7 insertions, 5 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index ef2f77069..e909a1f4f 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt = let mark_as_done pts = map_pftreestate (fun _ -> mark_proof_tree_as_done) - (traverse 0 pts) + (up_to_matching_rule is_focussing_command pts) (* post-instruction focus management *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6bf3e34b0..f9de72757 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -234,15 +234,17 @@ let add_hints_iff l2r lc n bl = Auto.add_hints true bl (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIff +VERNAC COMMAND EXTEND HintResolveIffLR [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff true lc n bl ] -| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] | [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] -> [ add_hints_iff true lc n ["core"] ] +END +VERNAC COMMAND EXTEND HintResolveIffRL + [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) + ":" preident_list(bl) ] -> + [ add_hints_iff false lc n bl ] | [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] -> [ add_hints_iff false lc n ["core"] ] END |