Merge PR #7677: [api] Remove Misctypes

12 files changed, 104 insertions, 37 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 450fcddfde..79b7e1599b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -26,7 +26,7 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Misctypes
+open Tactypes
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b85c4fc51b..f9506290a0 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open EConstr
 open Unification
-open Misctypes
+open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 38ed63c23d..544175c6d2 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -54,7 +54,7 @@ let clenv_cast_meta clenv =
 let clenv_value_cast_meta clenv =
     clenv_cast_meta clenv (clenv_value clenv)
 
-let clenv_pose_dependent_evars with_evars clenv =
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   let dep_mvs = clenv_dependent clenv in
   let env, sigma = clenv.env, clenv.evd in
   if not (List.is_empty dep_mvs) && not with_evars then
@@ -75,12 +75,12 @@ let check_tc evd =
   let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
   (has_typeclass, !has_resolvable)
 
-let clenv_refine with_evars ?(with_classes=true) clenv =
+let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
-  let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
       let (has_typeclass, has_resolvable) = check_tc clenv.evd in
@@ -105,10 +105,10 @@ open Unification
 
 let dft = default_unify_flags
 
-let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
+let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter begin fun gl ->
     let clenv = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes clenv
+    clenv_refine ?with_evars ~with_classes clenv
   end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 7c1e300b8f..d178478425 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -13,12 +13,11 @@
 open Clenv
 open EConstr
 open Unification
-open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
-val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
+val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
+val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
 
-val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 95c30d8159..e8ca719932 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -23,7 +23,6 @@ open Typing
 open Proof_type
 open Type_errors
 open Retyping
-open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -185,6 +184,22 @@ let check_decl_position env sigma sign d =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Printing of [move_location] *)
+
+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"
+
 let move_location_eq m1 m2 = match m1, m2 with
 | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
@@ -236,7 +251,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	      (first, d::middle)
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location Id.print hto ++
+                pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ Id.print hyp ++ str ".")
           else
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dc471bb5fe..9db54732bb 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+val pr_move_location :
+  ('a -> Pp.t) -> 'a move_location -> Pp.t
+
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
-  EConstr.named_declaration -> Id.t Misctypes.move_location ->
+  EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 1a63ff6734..ec17b8076f 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Names
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
   | IntroNaming p -> pr_intro_pattern_naming p
   | IntroAction p -> pr_intro_pattern_action prc p
 
-and pr_intro_pattern_naming = function
+and pr_intro_pattern_naming = let open Namegen in function
   | IntroIdentifier id -> Id.print id
   | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
@@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
 
-(** Printing of [move_location] *)
-
-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"
-
 (** Printing of bindings *)
 let pr_binding prc = let open CAst in function
   | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 79790a277b..f4e2e683d1 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,13 +18,10 @@ val pr_intro_pattern :
 val pr_or_and_intro_pattern :
   ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
 
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
+val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t
 
 (** Printing of [move_location] *)
 
-val pr_move_location :
-  ('a -> Pp.t) -> 'a move_location -> Pp.t
-
 val pr_bindings :
   ('a -> Pp.t) ->
   ('a -> Pp.t) -> 'a bindings -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9463793566..3120c97b58 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,7 +83,7 @@ type opacity_flag = Opaque | Transparent
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of opacity_flag *
-              Misctypes.lident option *
+              lident option *
               proof_object
 
 type proof_terminator = proof_ending -> unit
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0141cacb9e..9e07ed2d05 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.Id.t
 val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Misctypes.lident -> unit
+val discard : Names.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -54,7 +54,7 @@ type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
                 UState.t
   | Proved of opacity_flag *
-              Misctypes.lident option *
+              Names.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
@@ -126,7 +126,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Misctypes.lident list
+  Names.Id.t list -> Context.Named.t * Names.lident list
 val get_used_variables : unit -> Context.Named.t option
 
 (** Get the universe declaration associated to the current proof. *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 03ebc32759..629b77be2a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -23,7 +23,6 @@ open Tacred
 open CClosure
 open RedFlags
 open Libobject
-open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -200,8 +199,8 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
-  | ArgArg x -> x
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml
new file mode 100644
index 0000000000..86a7e9c527
--- /dev/null
+++ b/proofs/tactypes.ml
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Tactic-related types that are not totally Ltac specific and still used in
+    lower API. It's not clear whether this is a temporary API or if this is
+    meant to stay. *)
+
+open Names
+
+(** Introduction patterns *)
+
+type 'constr intro_pattern_expr =
+  | IntroForthcoming of bool
+  | IntroNaming of Namegen.intro_pattern_naming_expr
+  | IntroAction of 'constr intro_pattern_action_expr
+and 'constr intro_pattern_action_expr =
+  | IntroWildcard
+  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
+  | IntroRewrite of bool
+and 'constr or_and_intro_pattern_expr =
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
+
+(** Bindings *)
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
+
+type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
+
+type 'a bindings =
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_bindings
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
+
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
+
+type delayed_open_constr = EConstr.constr delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t