Tacexpr as a mli-only, the few functions there are now in Tacops

 NB: former Tacexpr.no_move is now Tacexpr.MoveLast
  (when introducing, intro with no move is intro as last)

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

5 files changed, 15 insertions, 14 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7cbcd584c9..55c03a481c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -22,7 +22,7 @@ open Misctypes
 open Locus
 open Decl_kinds
 
-let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
+let all_with delta = Tacops.make_red_flag [FBeta;FIota;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ; "by" ]
 let _ = List.iter Lexer.add_keyword tactic_kw
@@ -327,7 +327,7 @@ GEXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flag -> make_red_flag s
+    [ [ s = LIST1 red_flag -> Tacops.make_red_flag s
       | d = delta_flag -> all_with d
     ] ]
   ;
@@ -503,8 +503,8 @@ GEXTEND Gram
   move_location:
     [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
       | IDENT "before"; id = id_or_meta -> MoveBefore id
-      | "at"; IDENT "bottom" -> MoveToEnd true
-      | "at"; IDENT "top" -> MoveToEnd false ] ]
+      | "at"; IDENT "top" -> MoveFirst
+      | "at"; IDENT "bottom" -> MoveLast ] ]
   ;
   simple_tactic:
     [ [
@@ -515,8 +515,8 @@ GEXTEND Gram
       | IDENT "intro"; id = ident; hto = move_location ->
 	  TacIntroMove (Some id, hto)
       | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
-      | IDENT "intro"; id = ident -> TacIntroMove (Some id, no_move)
-      | IDENT "intro" -> TacIntroMove (None, no_move)
+      | IDENT "intro"; id = ident -> TacIntroMove (Some id, MoveLast)
+      | IDENT "intro" -> TacIntroMove (None, MoveLast)
 
       | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index cae4b13d68..caf3d8508a 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -69,7 +69,7 @@ Pattern
 Topconstr
 Genarg
 Ppextend
-Tacexpr
+Tacops
 Tok
 Lexer
 Extend
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c50ab9fcdb..58ce29a049 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -624,7 +624,7 @@ let pr_cofix_tac (id,c) =
   (* Printing tactics as arguments *)
 let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
-  | TacIntroMove (None,hto) when hto = no_move -> str "intro"
+  | TacIntroMove (None,MoveLast) -> str "intro"
   | TacAssumption -> str "assumption"
   | TacAnyConstructor (false,None) -> str "constructor"
   | TacAnyConstructor (true,None) -> str "econstructor"
@@ -647,10 +647,10 @@ and pr_atom1 = function
       hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
   | TacIntrosUntil h ->
       hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
-  | TacIntroMove (None,hto) as t when hto = no_move -> pr_atom0 t
-  | TacIntroMove (Some id,hto) when hto = no_move -> str "intro " ++ pr_id id
+  | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
+  | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
   | TacIntroMove (ido,hto) ->
-      hov 1 (str"intro" ++ pr_opt pr_id ido ++ pr_move_location pr_ident hto)
+      hov 1 (str"intro" ++ pr_opt pr_id ido ++ Tacops.pr_move_location pr_ident hto)
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +764,7 @@ and pr_atom1 = function
       assert b;
       hov 1
         (str "move" ++ brk (1,1) ++ pr_ident id1 ++
-	 pr_move_location pr_ident id2)
+	 Tacops.pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
         (str "rename" ++ brk (1,1) ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index b63e804d23..20fbda2d7f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -519,7 +519,7 @@ let pr_prim_rule = function
 
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
-	 str"move "  ++ pr_id id1 ++ pr_move_location pr_id id2)
+	 str"move "  ++ pr_id id1 ++ Tacops.pr_move_location pr_id id2)
 
   | Order ord ->
       (str"order "  ++ pr_sequence pr_id ord)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6ef7ba1d8a..c4581fe1e1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -238,7 +238,8 @@ let mlexpr_of_constr_with_binding =
 let mlexpr_of_move_location f = function
   | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >>
   | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >>
-  | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >>
+  | Tacexpr.MoveFirst -> <:expr< Tacexpr.MoveFirst >>
+  | Tacexpr.MoveLast -> <:expr< Tacexpr.MoveLast >>
 
 let mlexpr_of_induction_arg = function
   | Tacexpr.ElimOnConstr c ->