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, 70 insertions, 341 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index c7df86e1f7..3361752ed3 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 66001e77a5..6b8fbf24bc 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/tacexpr.ml b/proofs/tacexpr.ml
deleted file mode 100644
index 4f960243ca..0000000000
--- a/proofs/tacexpr.ml
+++ /dev/null
@@ -1,336 +0,0 @@
-(************************************************************************)
-(*  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 Pp
-open Util
-open Genarg
-open Pattern
-open Decl_kinds
-open Misctypes
-open Locus
-
-type 'a or_metaid = AI of 'a | MetaId of loc * string
-
-type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
-type lazy_flag = bool      (* true = lazy             false = eager *)
-type evars_flag = bool     (* true = pose evars       false = fail on evars *)
-type rec_flag = bool       (* true = recursive        false = not recursive *)
-type advanced_flag = bool  (* true = advanced         false = basic *)
-type split_flag = bool     (* true = exists           false = split *)
-type hidden_flag = bool    (* true = internal use     false = user-level *)
-type letin_flag = bool     (* true = use local def    false = use Leibniz *)
-
-type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
-
-type glob_red_flag =
-  | FBeta
-  | FIota
-  | FZeta
-  | 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")
-
-type 'a induction_arg =
-  | ElimOnConstr of 'a
-  | ElimOnIdent of identifier located
-  | ElimOnAnonHyp of int
-
-type inversion_kind =
-  | SimpleInversion
-  | FullInversion
-  | FullInversionClear
-
-type ('c,'id) inversion_strength =
-  | NonDepInversion of
-      inversion_kind * 'id list * intro_pattern_expr located option
-  | DepInversion of
-      inversion_kind * 'c option * intro_pattern_expr located option
-  | InversionUsing of 'c * 'id list
-
-type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
-
-type 'id message_token =
-  | MsgString of string
-  | MsgInt of int
-  | MsgIdent of 'id
-
-type 'constr induction_clause =
-  ('constr with_bindings induction_arg list * 'constr with_bindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option))
-
-type ('constr,'id) induction_clause_list =
-    'constr induction_clause list * 'id clause_expr option
-
-type multi =
-  | Precisely of int
-  | UpTo of int
-  | RepeatStar
-  | RepeatPlus
-
-(* Type of patterns *)
-type 'a match_pattern =
-  | Term of 'a
-  | Subterm of bool * identifier option * 'a
-
-(* Type of hypotheses for a Match Context rule *)
-type 'a match_context_hyps =
-  | Hyp of name located * 'a match_pattern
-  | Def of name located * 'a match_pattern * 'a match_pattern
-
-(* Type of a Match rule for Match Context and Match *)
-type ('a,'t) match_rule =
-  | Pat of 'a match_context_hyps list * 'a match_pattern * 't
-  | All of 't
-
-type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
-  (* Basic tactics *)
-  | TacIntroPattern of intro_pattern_expr located list
-  | TacIntrosUntil of quantified_hypothesis
-  | TacIntroMove of identifier option * 'id move_location
-  | TacAssumption
-  | TacExact of 'constr
-  | TacExactNoCheck of 'constr
-  | TacVmCastNoCheck of 'constr
-  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
-      ('id * intro_pattern_expr located option) option
-  | TacElim of evars_flag * 'constr with_bindings *
-      'constr with_bindings option
-  | TacElimType of 'constr
-  | TacCase of evars_flag * 'constr with_bindings
-  | TacCaseType of 'constr
-  | TacFix of identifier option * int
-  | TacMutualFix of hidden_flag * identifier * int * (identifier * int *
-      'constr) list
-  | TacCofix of identifier option
-  | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
-  | TacCut of 'constr
-  | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
-  | TacGeneralize of ('constr with_occurrences * name) list
-  | TacGeneralizeDep of 'constr
-  | TacLetTac of name * 'constr * 'id clause_expr * letin_flag
-
-  (* Derived basic tactics *)
-  | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
-  | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause_list
-  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
-  | TacDecomposeAnd of 'constr
-  | TacDecomposeOr of 'constr
-  | TacDecompose of 'ind list * 'constr
-  | TacSpecialize of int option * 'constr with_bindings
-  | TacLApply of 'constr
-
-  (* Automation tactics *)
-  | TacTrivial of debug * 'constr list * string list option
-  | TacAuto of debug * int or_var option * 'constr list * string list option
-
-  (* Context management *)
-  | TacClear of bool * 'id list
-  | TacClearBody of 'id list
-  | TacMove of bool * 'id * 'id move_location
-  | TacRename of ('id *'id) list
-  | TacRevert of 'id list
-
-  (* Constructors *)
-  | TacLeft of evars_flag * 'constr bindings
-  | TacRight of evars_flag * 'constr bindings
-  | TacSplit of evars_flag * split_flag * 'constr bindings list
-  | TacAnyConstructor of evars_flag * 'tac option
-  | TacConstructor of evars_flag * int or_var * 'constr bindings
-
-  (* Conversion *)
-  | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id clause_expr
-  | TacChange of 'pat option * 'constr * 'id clause_expr
-
-  (* Equivalence relations *)
-  | TacReflexivity
-  | TacSymmetry of 'id clause_expr
-  | TacTransitivity of 'constr option
-
-  (* Equality and inversion *)
-  | TacRewrite of
-      evars_flag * (bool * multi * 'constr with_bindings) list * 'id clause_expr * 'tac option
-  | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
-
-  (* For ML extensions *)
-  | TacExtend of loc * string * 'lev generic_argument list
-
-  (* For syntax extensions *)
-  | TacAlias of loc * string *
-      (identifier * 'lev generic_argument) list
-      * (dir_path * glob_tactic_expr)
-
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
-  | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr
-  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
-	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array *
-	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
-	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array
-  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
-	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
-  | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
-  | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
-  | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option
-  | TacId of 'id message_token list
-  | TacFail of int or_var * 'id message_token list
-  | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-  | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
-  | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
-  | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast
-  | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located
-
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast =
-  identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
-
-  (* These are the possible arguments of a tactic definition *)
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
-  | TacDynamic     of loc * Dyn.t
-  | TacVoid
-  | MetaIdArg      of loc * bool * string
-  | ConstrMayEval  of ('constr,'cst,'pat) may_eval
-  | IntroPattern   of intro_pattern_expr located
-  | Reference      of 'ref
-  | Integer        of int
-  | TacCall        of loc *
-      'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
-  | TacExternal of loc * string * string *
-      ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
-  | TacFreshId     of string or_var list
-  | Tacexp of 'tac
-
-(* Globalized tactics *)
-and glob_tactic_expr =
-    (glob_constr_and_expr,
-     glob_constr_and_expr * constr_pattern,
-     evaluable_global_reference and_short_name or_var,
-     inductive or_var,
-     ltac_constant located or_var,
-     identifier located,
-     glob_tactic_expr,
-     glevel) gen_tactic_expr
-
-type raw_tactic_expr =
-    (constr_expr,
-     constr_pattern_expr,
-     reference or_by_notation,
-     reference or_by_notation,
-     reference,
-     identifier located or_metaid,
-     raw_tactic_expr,
-     rlevel) gen_tactic_expr
-
-type raw_atomic_tactic_expr =
-    (constr_expr,                  (* constr *)
-     constr_pattern_expr,                 (* pattern *)
-     reference or_by_notation,     (* evaluable reference *)
-     reference or_by_notation,     (* inductive *)
-     reference,                    (* ltac reference *)
-     identifier located or_metaid, (* identifier *)
-     raw_tactic_expr,
-     rlevel) gen_atomic_tactic_expr
-
-type raw_tactic_arg =
-    (constr_expr,
-     constr_pattern_expr,
-     reference or_by_notation,
-     reference or_by_notation,
-     reference,
-     identifier located or_metaid,
-     raw_tactic_expr,
-     rlevel) gen_tactic_arg
-
-type raw_generic_argument = rlevel generic_argument
-
-type raw_red_expr =
-    (constr_expr, reference or_by_notation, constr_expr) red_expr_gen
-
-type glob_atomic_tactic_expr =
-    (glob_constr_and_expr,
-     glob_constr_and_expr * constr_pattern,
-     evaluable_global_reference and_short_name or_var,
-     inductive or_var,
-     ltac_constant located or_var,
-     identifier located,
-     glob_tactic_expr,
-     glevel) gen_atomic_tactic_expr
-
-type glob_tactic_arg =
-    (glob_constr_and_expr,
-     glob_constr_and_expr * constr_pattern,
-     evaluable_global_reference and_short_name or_var,
-     inductive or_var,
-     ltac_constant located or_var,
-     identifier located,
-     glob_tactic_expr,
-     glevel) gen_tactic_arg
-
-type glob_generic_argument = glevel generic_argument
-
-type glob_red_expr =
-    (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern)
-    red_expr_gen
-
-type typed_generic_argument = tlevel generic_argument
-
-type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
-
-type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
-
-type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
-
-type 'a declaration_hook = locality -> global_reference -> 'a
diff --git a/proofs/tacops.ml b/proofs/tacops.ml
new file mode 100644
index 0000000000..05c4e60934
--- /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 0000000000..be17e035a9
--- /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