[api] Misctypes removal: tactic flags.

We move the "flag types" to its use place, and mark some arguments
with named parameters better.

9 files changed, 25 insertions, 19 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/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/equality.ml b/tactics/equality.ml
index 1033c56c9..671e765e0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -155,7 +155,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 =
@@ -1044,7 +1044,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 9395cf4a8..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 *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 53a02f89b..f34c83ae7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -223,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 ->
@@ -231,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
@@ -634,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
@@ -663,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' =
@@ -686,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 cf07532c0..67170d2cf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,7 +43,6 @@ open Pretype_errors
 open Unification
 open Locus
 open Locusops
-open Misctypes
 open Tactypes
 open Proofview.Notations
 open Context.Named.Declaration
@@ -1154,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
@@ -1282,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 
@@ -2259,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
@@ -4197,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 086442e42..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
@@ -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 *)