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

18 files changed, 130 insertions, 93 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 8ba207000..436fa287f 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -115,7 +115,7 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
-Tacexpr
+Tacops
 Proof_type
 Goal
 Logic
diff --git a/proofs/tacexpr.ml b/intf/tacexpr.mli
index 4f960243c..16ba9f95e 100644
--- a/proofs/tacexpr.ml
+++ b/intf/tacexpr.mli
@@ -40,43 +40,13 @@ type glob_red_flag =
   | FConst of reference or_by_notation list
   | FDeltaBut of reference or_by_notation list
 
-let make_red_flag =
-  let rec add_flag red = function
-    | [] -> red
-    | FBeta :: lf -> add_flag { red with rBeta = true } lf
-    | FIota :: lf -> add_flag { red with rIota = true } lf
-    | FZeta :: lf -> add_flag { red with rZeta = true } lf
-    | FConst l :: lf ->
-	if red.rDelta then
-	  error
-	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag { red with rConst = list_union red.rConst l } lf
-    | FDeltaBut l :: lf ->
-	if red.rConst <> [] & not red.rDelta then
-	  error
-	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag
-	  { red with rConst = list_union red.rConst l; rDelta = true }
-	  lf
-  in
-  add_flag
-    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
-
 type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
 
 type 'id move_location =
   | MoveAfter of 'id
   | MoveBefore of 'id
-  | MoveToEnd of bool
-
-let no_move = MoveToEnd true
-
-open Pp
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top")
+  | MoveFirst
+  | MoveLast (* can be seen as "no move" when doing intro *)
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7cbcd584c..55c03a481 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 cae4b13d6..caf3d8508 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 c50ab9fcd..58ce29a04 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 b63e804d2..20fbda2d7 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 6ef7ba1d8..c4581fe1e 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 ->
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 21058a7b9..a45b8cda4 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -96,7 +96,6 @@ let
  let module PT = Proof_type in
  let module L = Logic in
  let module X = Xml in
- let module T = Tacexpr in
   let ids_of_node node =
    let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
 (*
@@ -144,7 +143,7 @@ Pp.ppnl (Pp.(++) (Pp.str
          Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
         in begin
         match tactic_expr with
-        | T.TacArg (_,T.Tacexp _) ->
+        | Tacexpr.TacArg (_,Tacexpr.Tacexp _) ->
             (* We don't need to keep the level of abstraction introduced at *)
             (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
             aux flat_proof old_hyps
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c7df86e1f..3361752ed 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -221,7 +221,7 @@ let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
   | (hyp,_,_) :: right ->
       if hyp = h then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false
+	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
       else
        get_hyp_after h right
 
@@ -230,7 +230,7 @@ let split_sign hfrom hto l =
     | [] -> error_no_such_hypothesis hfrom
     | (hyp,c,typ) as d :: right ->
       	if hyp = hfrom then
-	  (left,right,d, toleft or hto = MoveToEnd true)
+	  (left,right,d, toleft or hto = MoveLast)
       	else
 	  splitrec (d::left)
 	    (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
@@ -252,7 +252,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   in
   let rec moverec first middle = function
     | [] ->
-	if match hto with MoveToEnd _ -> false | _ -> true then
+	if match hto with MoveFirst | MoveLast -> false | _ -> true then
 	  error_no_such_hypothesis (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
     | (hyp,_,_) :: _ as right when hto = MoveBefore hyp ->
@@ -264,7 +264,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	      (first, d::middle)
             else
 	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
-	        pr_move_location pr_id hto ++
+	        Tacops.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
           else
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 66001e77a..6b8fbf24b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -3,7 +3,7 @@ Evar_refiner
 Proofview
 Proof
 Proof_global
-Tacexpr
+Tacops
 Proof_type
 Redexpr
 Logic
diff --git a/proofs/tacops.ml b/proofs/tacops.ml
new file mode 100644
index 000000000..05c4e6093
--- /dev/null
+++ b/proofs/tacops.ml
@@ -0,0 +1,51 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Topconstr
+open Libnames
+open Nametab
+open Glob_term
+open Errors
+open Util
+open Genarg
+open Pattern
+open Decl_kinds
+open Misctypes
+open Locus
+open Tacexpr
+
+let make_red_flag =
+  let rec add_flag red = function
+    | [] -> red
+    | FBeta :: lf -> add_flag { red with rBeta = true } lf
+    | FIota :: lf -> add_flag { red with rIota = true } lf
+    | FZeta :: lf -> add_flag { red with rZeta = true } lf
+    | FConst l :: lf ->
+	if red.rDelta then
+	  error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag { red with rConst = list_union red.rConst l } lf
+    | FDeltaBut l :: lf ->
+	if red.rConst <> [] & not red.rDelta then
+	  error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag
+	  { red with rConst = list_union red.rConst l; rDelta = true }
+	  lf
+  in
+  add_flag
+    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
+
+open Pp
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
diff --git a/proofs/tacops.mli b/proofs/tacops.mli
new file mode 100644
index 000000000..be17e035a
--- /dev/null
+++ b/proofs/tacops.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val make_red_flag :
+ Tacexpr.glob_red_flag list ->
+ (Libnames.reference Misctypes.or_by_notation) Glob_term.glob_red_flag
+
+val pr_move_location :
+  ('a -> Pp.std_ppcmds) -> 'a Tacexpr.move_location -> Pp.std_ppcmds
diff --git a/tactics/elim.ml b/tactics/elim.ml
index aa13d27b1..bd304d975 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -49,7 +49,7 @@ let introCaseAssumsThen tac ba =
       (ba.branchnames, []),
        if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
   let introCaseAssums =
-    tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in
+    tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
 (* The following tactic Decompose repeatedly applies the
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 03f3811b7..cfbb30a74 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1160,7 +1160,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
             ) else (raise Not_dep_pair)
         ) with _ ->
 	  inject_at_positions env sigma u eq_clause posns
-	    (fun _ -> intros_pattern no_move ipats)
+	    (fun _ -> intros_pattern MoveLast ipats)
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8410e08cc..d1d3d90c5 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -22,7 +22,7 @@ open Misctypes
 (* Basic tactics *)
 let h_intro_move x y =
   abstract_tactic (TacIntroMove (x, y)) (intro_move x y)
-let h_intro x        = h_intro_move (Some x) no_move
+let h_intro x        = h_intro_move (Some x) MoveLast
 let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
 let h_exact c        = abstract_tactic (TacExact c) (exact_check c)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f5762768e..f1f844076 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -295,7 +295,7 @@ let rec tclMAP_i n tacfun = function
       if n=0 then error "Too many names."
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
-let remember_first_eq id x = if !x = no_move then x := MoveAfter id
+let remember_first_eq id x = if !x = MoveLast then x := MoveAfter id
 
 (* invariant: ProjectAndApply is responsible for erasing the clause
    which it is given as input
@@ -322,7 +322,7 @@ let projectAndApply thin id eqname names depids gls =
       [(if names <> [] then clear [id] else tclIDTAC);
        (tclMAP_i neqns (fun idopt ->
 	 tclTRY (tclTHEN
-	   (intro_move idopt no_move)
+	   (intro_move idopt MoveLast)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
 	   (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))))
@@ -353,7 +353,7 @@ let rewrite_equations_gene othin neqns ba gl =
                         (onLastHypId
                            (fun id ->
                               tclTRY
-			        (projectAndApply thin id (ref no_move)
+			        (projectAndApply thin id (ref MoveLast)
 				  [] depids))));
                  onHyps (compose List.rev (afterHyp last)) bring_hyps;
                  onHyps (afterHyp last)
@@ -407,7 +407,7 @@ let rewrite_equations othin neqns names ba gl =
   let names = List.map (get_names true) names in
   let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
   let rewrite_eqns =
-    let first_eq = ref no_move in
+    let first_eq = ref MoveLast in
     match othin with
       | Some thin ->
           tclTHENSEQ
@@ -416,12 +416,12 @@ let rewrite_equations othin neqns names ba gl =
 	     tclMAP_i neqns (fun o ->
 	       let idopt,names = extract_eqn_names o in
                (tclTHEN
-		 (intro_move idopt no_move)
+		 (intro_move idopt MoveLast)
 		 (onLastHypId (fun id ->
 		   tclTRY (projectAndApply thin id first_eq names depids)))))
 	       names;
 	     tclMAP (fun (id,_,_) gl ->
-	       intro_move None (if thin then no_move else !first_eq) gl)
+	       intro_move None (if thin then MoveLast else !first_eq) gl)
 	       nodepids;
 	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
       | None -> tclIDTAC
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0d277855f..f3b6c58c0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -173,7 +173,7 @@ let _ =
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl None,nocl);
         "compute", TacReduce(Cbv all_flags,nocl);
-        "intro", TacIntroMove(None,no_move);
+        "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
         "assumption", TacAssumption;
         "cofix", TacCofix None;
@@ -384,7 +384,8 @@ let intern_constr_reference strict ist = function
 let intern_move_location ist = function
   | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id)
   | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id)
-  | MoveToEnd toleft as x -> x
+  | MoveFirst -> MoveFirst
+  | MoveLast -> MoveLast
 
 (* Internalize an isolated reference in position of tactic *)
 
@@ -1130,7 +1131,8 @@ let interp_hyp_list ist gl l =
 let interp_move_location ist gl = function
   | MoveAfter id -> MoveAfter (interp_hyp ist gl id)
   | MoveBefore id -> MoveBefore (interp_hyp ist gl id)
-  | MoveToEnd toleft as x -> x
+  | MoveFirst -> MoveFirst
+  | MoveLast -> MoveLast
 
 (* Interprets a qualified name *)
 let coerce_to_reference env v =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e350bfe9..897e1d7ef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -425,7 +425,7 @@ let find_intro_names ctxt gl =
   List.rev res
 
 let build_intro_tac id dest tac = match dest with
-  | MoveToEnd true -> tclTHEN (introduction id) (tac id)
+  | MoveLast -> tclTHEN (introduction id) (tac id)
   | dest -> tclTHENLIST [introduction id; move_hyp true id dest; tac id]
 
 let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
@@ -444,14 +444,14 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
 	  user_err_loc(loc,"Intro",str "No product even after head-reduction.")
 
 let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC)
-let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true false
-let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false
-let intro_then = intro_then_gen dloc (IntroAvoid []) no_move false false
-let intro = intro_gen dloc (IntroAvoid []) no_move false false
-let introf = intro_gen dloc (IntroAvoid []) no_move true false
-let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false
+let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
+let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) MoveLast false false
+let intro_then = intro_then_gen dloc (IntroAvoid []) MoveLast false false
+let intro = intro_gen dloc (IntroAvoid []) MoveLast false false
+let introf = intro_gen dloc (IntroAvoid []) MoveLast true false
+let intro_avoiding l = intro_gen dloc (IntroAvoid l) MoveLast false false
 
-let intro_then_force = intro_then_gen dloc (IntroAvoid []) no_move true false
+let intro_then_force = intro_then_gen dloc (IntroAvoid []) MoveLast true false
 
 (**** Multiple introduction tactics ****)
 
@@ -475,7 +475,7 @@ let rec get_next_hyp_position id = function
   | [] -> error ("No such hypothesis: " ^ string_of_id id)
   | (hyp,_,_) :: right ->
       if hyp = id then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd true
+	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
       else
 	get_next_hyp_position id right
 
@@ -1362,7 +1362,7 @@ let check_thin_clash_then id thin avoid tac =
 let rec intros_patterns b avoid ids thin destopt tac = function
   | (loc, IntroWildcard) :: l ->
       intro_then_gen loc (IntroBasedOn(wild_id,avoid@explicit_intro_names l))
-	no_move true false
+	MoveLast true false
         (fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt tac l)
   | (loc, IntroIdentifier id) :: l ->
       check_thin_clash_then id thin avoid (fun thin ->
@@ -1387,7 +1387,7 @@ let rec intros_patterns b avoid ids thin destopt tac = function
 	   (intros_patterns b avoid ids thin destopt tac))
   | (loc, IntroRewrite l2r) :: l ->
       intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
-	no_move true false
+	MoveLast true false
         (fun id ->
 	  tclTHENLAST (* Skip the side conditions of the rewriting step *)
 	    (rewrite_hyp l2r id)
@@ -1402,7 +1402,7 @@ let intro_pattern destopt pat =
 
 let intro_patterns = function
   | [] -> tclREPEAT intro
-  | l  -> intros_pattern no_move l
+  | l  -> intros_pattern MoveLast l
 
 (**************************)
 (*   Other cut tactics    *)
@@ -1423,7 +1423,7 @@ let prepare_intros s ipat gl = match ipat with
   | IntroOrAndPattern ll -> make_id s gl,
       onLastHypId
 	(intro_or_and_pattern loc true ll []
-	  (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards)))
+	  (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards)))
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected")
 
@@ -1457,7 +1457,7 @@ let as_tac id ipat = match ipat with
       !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll []
-        (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards))
+        (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards))
         id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
@@ -1748,7 +1748,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
     | Some occ ->
         subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
   let lastlhyp =
-    if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
+    if depdecls = [] then MoveLast else MoveAfter(pi1(list_last depdecls)) in
   (depdecls,lastlhyp,ccl,out test)
 
 let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
@@ -1895,15 +1895,15 @@ let rec consume_pattern avoid id isdep gl = function
   | pat::names -> (pat,names)
 
 let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
-  let tophyp = match tophyp with None -> MoveToEnd true | Some hyp -> MoveAfter hyp in
+  let tophyp = match tophyp with None -> MoveLast | Some hyp -> MoveAfter hyp in
   let newlstatus = (* if some IH has taken place at the top of hyps *)
-    List.map (function (hyp,MoveToEnd true) -> (hyp,tophyp) | x -> x) lstatus
+    List.map (function (hyp,MoveLast) -> (hyp,tophyp) | x -> x) lstatus
   in
   tclTHEN
     (intros_move rstatus)
     (intros_move newlstatus)
 
-let update destopt tophyp = if destopt = no_move then tophyp else destopt
+let update destopt tophyp = if destopt = MoveLast then tophyp else destopt
 
 let safe_dest_intros_patterns avoid thin dest pat tac gl =
   try intros_patterns true avoid [] thin dest tac pat gl
@@ -1912,7 +1912,7 @@ let safe_dest_intros_patterns avoid thin dest pat tac gl =
        only after cook_sign is called, e.g. as in "destruct dec" in context
        "dec:forall x, {x=0}+{x<>0};  a:A  |- if dec a then True else False"
        where argument a of dec will be found only lately *)
-    intros_patterns true avoid [] [] no_move tac pat gl
+    intros_patterns true avoid [] [] MoveLast tac pat gl
 
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
@@ -1929,7 +1929,7 @@ let update_dest (recargdests,tophyp as dests) = function
 
 let get_recarg_dest (recargdests,tophyp) =
   match recargdests with
-  | AfterFixedPosition None -> MoveToEnd true
+  | AfterFixedPosition None -> MoveLast
   | AfterFixedPosition (Some id) -> MoveAfter id
 
 (* Current policy re-introduces recursive arguments of destructed
@@ -1956,13 +1956,13 @@ let induct_discharge dests avoid' tac (avoid,ra) names gl =
         let hyprec,names = consume_pattern avoid hyprecname depind gl names in
         let dest = get_recarg_dest dests in
         safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
-	safe_dest_intros_patterns avoid thin no_move [hyprec] (fun ids' thin ->
+	safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
 	peel_tac ra' (update_dest dests ids') names thin))
           gl
     | (IndArg,dep,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names = consume_pattern avoid hyprecname dep gl names in
-	safe_dest_intros_patterns avoid thin no_move [pat] (fun ids thin ->
+	safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin) gl
     | (RecArg,dep,recvarname) :: ra' ->
         let pat,names = consume_pattern avoid recvarname dep gl names in
@@ -2123,7 +2123,7 @@ let cook_sign hyp0_opt indvars env =
       (* If there was no main induction hypotheses, then hyp is one of
          indvars too, so add it to indhyps. *)
       (if hyp0_opt=None then indhyps := hyp::!indhyps);
-      MoveToEnd false (* fake value *)
+      MoveFirst (* fake value *)
     end else if List.mem hyp indvars then begin
       (* warning: hyp can still occur after induction *)
       (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *)
@@ -2143,7 +2143,7 @@ let cook_sign hyp0_opt indvars env =
       else
 	MoveBefore hyp
   in
-  let _ = fold_named_context seek_deps env ~init:(MoveToEnd false) in
+  let _ = fold_named_context seek_deps env ~init:MoveFirst in
   (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
   let compute_lstatus lhyp (hyp,_,_) =
     if hyp = hyp0 then raise (Shunt lhyp);
@@ -2155,11 +2155,11 @@ let cook_sign hyp0_opt indvars env =
   in
   try
     let _ =
-      fold_named_context_reverse compute_lstatus ~init:(MoveToEnd true) env in
-    raise (Shunt (MoveToEnd true)) (* ?? FIXME *)
+      fold_named_context_reverse compute_lstatus ~init:MoveLast env in
+    raise (Shunt MoveLast) (* ?? FIXME *)
   with Shunt lhyp0 ->
     let lhyp0 = match lhyp0 with
-      | MoveToEnd true -> None
+      | MoveLast -> None
       | MoveAfter hyp -> Some hyp
       | _ -> assert false in
     let statuslists = (!lstatus,List.rev !rstatus) in