Merge PR #7677: [api] Remove Misctypes

16 files changed, 62 insertions, 47 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 77fe31415..d7de6c4fb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
-  Clenvtac.clenv_refine false clenv
+  Clenvtac.clenv_refine clenv
   end
 
 let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4beeaaae0..773fc1520 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -207,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
       with e -> Proofview.tclZERO e
     in resolve >>= fun clenv' ->
-       Clenvtac.clenv_refine with_evars ~with_classes:false clenv'
+       Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
 
 let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b92bc75bc..e12063fd4 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -14,7 +14,6 @@ open Hipattern
 open Tactics
 open Coqlib
 open Reductionops
-open Misctypes
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) =
     else
       Proofview.tclORELSE
         begin
-          if lbind = NoBindings then
+          if lbind = Tactypes.NoBindings then
             filter_hyp (fun c -> is_negation_of env sigma typ c)
               (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
           else
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 2b3a94758..4bb3263fb 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open EConstr
-open Misctypes
+open Tactypes
 
 val absurd                      : constr -> unit Proofview.tactic
 val contradiction               : constr with_bindings option -> unit Proofview.tactic
diff --git a/tactics/elim.mli b/tactics/elim.mli
index d6b67e5ba..ddfac3f2c 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -11,12 +11,11 @@
 open Names
 open EConstr
 open Tacticals
-open Misctypes
 open Tactypes
 
 (** Eliminations tactics. *)
 
-val introCaseAssumsThen : evars_flag ->
+val introCaseAssumsThen : Tactics.evars_flag ->
   (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 176701d99..832014a61 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -24,11 +24,11 @@ open Tactics
 open Tacticals.New
 open Auto
 open Constr_matching
-open Misctypes
 open Hipattern
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
+open Tactypes
 
 (* This file containts the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
@@ -58,14 +58,14 @@ let clear_last =
 
 let choose_eq eqonleft =
   if eqonleft then
-    left_with_bindings false Misctypes.NoBindings
+    left_with_bindings false NoBindings
   else
-    right_with_bindings false Misctypes.NoBindings
+    right_with_bindings false NoBindings
 let choose_noteq eqonleft =
   if eqonleft then
-    right_with_bindings false Misctypes.NoBindings
+    right_with_bindings false NoBindings
   else
-    left_with_bindings false Misctypes.NoBindings
+    left_with_bindings false NoBindings
 
 (* A surgical generalize which selects the right occurrences by hand *)
 (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d7e697aed..91c577405 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -42,7 +42,7 @@ open Ind_tables
 open Eqschemes
 open Locus
 open Locusops
-open Misctypes
+open Tactypes
 open Proofview.Notations
 open Unification
 open Context.Named.Declaration
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
-    Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
+    Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
   in
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
@@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
@@ -1037,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) =
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
-  let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
+  let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ccf454c3e..6f3e08ea0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -15,8 +15,8 @@ open EConstr
 open Environ
 open Ind_tables
 open Locus
-open Misctypes
 open Tactypes
+open Tactics
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
@@ -61,6 +61,12 @@ val general_rewrite_in          :
 val general_rewrite_clause :
   orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 val general_multi_rewrite :
   evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5d264058a..f9c4bed35 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,7 @@ open Evar_kinds
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
 let mkGApp f args = DAst.make @@ GApp (f, args)
 let mkGHole = DAst.make @@
-  GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
+  GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None)
 let mkGProd id c1 c2 = DAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
 let mkGArrow c1 c2 = DAst.make @@
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 102b8e54d..755494c2d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -26,7 +26,7 @@ open Tacticals.New
 open Tactics
 open Elim
 open Equality
-open Misctypes
+open Tactypes
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -332,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function
           (tacfun (get_names allow_conj a))
           (tclMAP_i allow_conj (n-1) tacfun l)
 
-let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
+let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id
 
 (* invariant: ProjectAndApply is responsible for erasing the clause
    which it is given as input
@@ -375,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
       [if as_mode then clear [id] else tclIDTAC;
        (tclMAP_i (false,false) neqns (function (idopt,_) ->
 	 tclTRY (tclTHEN
-	   (intro_move_avoid idopt avoid MoveLast)
+           (intro_move_avoid idopt avoid Logic.MoveLast)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
 	   (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
@@ -404,7 +404,7 @@ let nLastDecls i tac =
 let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.enter begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
-  let first_eq = ref MoveLast in
+  let first_eq = ref Logic.MoveLast in
   let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
   match othin with
     | Some thin ->
@@ -416,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba =
              (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
 	     tclMAP_i (true,false) neqns (fun (idopt,names) ->
                (tclTHEN
-		 (intro_move_avoid idopt avoid MoveLast)
+                 (intro_move_avoid idopt avoid Logic.MoveLast)
 		 (onLastHypId (fun id ->
 		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
 	     tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
                let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
-	       intro_move idopt (if thin then MoveLast else !first_eq))
+               intro_move idopt (if thin then Logic.MoveLast else !first_eq))
 	       nodepids;
 	     (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
     | None ->
         (* simple inversion *)
         if as_mode then
           tclMAP_i (false,true) neqns (fun (idopt,_) ->
-	    intro_move idopt MoveLast) names
+            intro_move idopt Logic.MoveLast) names
         else
           (tclTHENLIST
              [tclDO neqns intro;
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 9d4ffdd7b..bbd1f3352 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Misctypes
 open Tactypes
 
 type inversion_status = Dep of constr option | NoDep
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 2337a7901..f42e5a8b0 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -11,7 +11,7 @@
 open Names
 open EConstr
 open Constrexpr
-open Misctypes
+open Tactypes
 
 val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 732d06f8a..f34c83ae7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -159,8 +159,6 @@ type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
-open Misctypes
-
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
@@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
         if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
         if Int.equal p p1 then
           IntroAndPattern
-            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
+            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l)
         else
           names
       else
@@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function
 let compute_induction_names = compute_induction_names_gen true
 
 (* Compute the let-in signature of case analysis or standard induction scheme *)
-let compute_constructor_signatures isrec ((_,k as ity),u) =
+let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
     match Constr.kind c, recargs with
     | Prod (_,_,c), recarg::rest ->
@@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
         begin match Declareops.dest_recarg recarg with
         | Norec | Imbr _  -> true :: rest
         | Mrec (_,j)  ->
-            if isrec && Int.equal j k then true :: true :: rest
+            if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
         end
     | LetIn (_,_,_,c), rest -> false :: analrec c rest
@@ -636,7 +634,7 @@ module New = struct
   (* Find the right elimination suffix corresponding to the sort of the goal *)
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
-      isrec allnames tac predicate ind (c, t) =
+      rec_flag allnames tac predicate ind (c, t) =
     Proofview.Goal.enter begin fun gl ->
     let sigma, elim = mk_elim ind gl in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -665,7 +663,7 @@ module New = struct
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_constructor_signatures isrec ind in
+    let branchsigns = compute_constructor_signatures ~rec_flag ind in
     let brnames = compute_induction_names_gen false branchsigns allnames in
     let flags = Unification.elim_flags () in
     let elimclause' =
@@ -688,7 +686,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Clenvtac.clenv_refine false clenv')
+      (Clenvtac.clenv_refine clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end) end
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cbaf691f1..1e66c2b0b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -14,7 +14,6 @@ open EConstr
 open Evd
 open Proof_type
 open Locus
-open Misctypes
 open Tactypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
@@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int ->
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
-val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
+val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d..67170d2cf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,7 +43,7 @@ open Pretype_errors
 open Unification
 open Locus
 open Locusops
-open Misctypes
+open Tactypes
 open Proofview.Notations
 open Context.Named.Declaration
 
@@ -1153,6 +1153,11 @@ let tactic_infer_flags with_evar = {
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
+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 clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
 type 'a core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of lident
@@ -1281,7 +1286,7 @@ let do_replace id = function
 
 let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) 
     targetid id sigma0 clenv tac =
-  let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
+  let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
   let clenv =
     if with_classes then
       { clenv with evd = Typeclasses.resolve_typeclasses 
@@ -2258,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let branchsigns = compute_constructor_signatures false ind in
+  let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
   let nv_with_let = Array.map List.length branchsigns in
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
@@ -4196,7 +4201,7 @@ let induction_tac with_evars params indvars elim =
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  Clenvtac.clenv_refine with_evars resolved
+  Clenvtac.clenv_refine ~with_evars resolved
   end
 
 (* Apply induction "in place" taking into account dependent
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b17330f13..8d4302450 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -18,7 +18,6 @@ open Clenv
 open Redexpr
 open Pattern
 open Unification
-open Misctypes
 open Tactypes
 open Locus
 open Ltac_pretype
@@ -56,8 +55,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
-val intro_move        : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val intro_move_avoid  : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic
+val intro_move        : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic
+val intro_move_avoid  : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic
 
   (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
@@ -91,6 +90,11 @@ val intros_clearing      : bool list -> unit Proofview.tactic
 val try_intros_until :
   (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic
 
+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 clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
 (** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
@@ -117,11 +121,11 @@ val use_clear_hyp_by_default : unit -> bool
 (** {6 Introduction tactics with eliminations. } *)
 
 val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
+val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr ->
   unit Proofview.tactic
 
 (** Implements user-level "intros", with [] standing for "**" *)
@@ -188,7 +192,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> intro_pattern option -> unit Proofview.tactic
 
-val move_hyp      : Id.t -> Id.t move_location -> unit Proofview.tactic
+val move_hyp      : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic