- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses

- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 6 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index bd9e1f7f3..9b5c14f23 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1155,17 +1155,23 @@ and xlate_tac =
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
+    | TacLetTac (na, c, cl) when cl = nowhere -> 
+        CT_pose(xlate_id_opt_aux na, xlate_formula c)
     | TacLetTac (na, c, cl) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
-    | TacForward (true, name, c) -> 
-               CT_pose(xlate_id_opt_aux name, xlate_formula c)
-    | TacForward (false, name, c) -> 
-               CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
-    | TacTrueCut (na, c) -> 
-        CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
+    | TacAssert (None, Some (IntroIdentifier id), c) -> 
+        CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (None, None, c) -> 
+        CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert (Some (TacId ""), Some (IntroIdentifier id), c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (Some (TacId ""), None, c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert _ ->
+	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
     | TacAnyConstructor(Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))