Moving Ftactic and Geninterp to the engine folder.

5 files changed, 0 insertions, 249 deletions

diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
deleted file mode 100644
index 588709873..000000000
--- a/tactics/ftactic.ml
+++ /dev/null
@@ -1,106 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Proofview.Notations
-
-(** Focussing tactics *)
-
-type 'a focus =
-| Uniform of 'a
-| Depends of 'a list
-
-(** Type of tactics potentially goal-dependent. If it contains a [Depends],
-    then the length of the inner list is guaranteed to be the number of
-    currently focussed goals. Otherwise it means the tactic does not depend
-    on the current set of focussed goals. *)
-type 'a t = 'a focus Proofview.tactic
-
-let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x)
-
-let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
-| Uniform x -> f x
-| Depends l ->
-  let f arg = f arg >>= function
-  | Uniform x ->
-    (** We dispatch the uniform result on each goal under focus, as we know
-        that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
-    Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
-  in
-  Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
-
-let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-let set_sigma r =
-  let Sigma.Sigma (ans, sigma, _) = r in
-  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () -> ans
-
-let nf_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f.enter nfgl))
-
-let nf_s_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter nfgl)))
-
-let enter f =
-  bind goals
-    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f.enter gl))
-
-let s_enter f =
-  bind goals
-    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter gl)))
-
-let with_env t =
-  t >>= function
-    | Uniform a ->
-        Proofview.tclENV >>= fun env -> Proofview.tclUNIT (Uniform (env,a))
-    | Depends l ->
-        Proofview.Goal.goals >>= fun gs ->
-        Proofview.Monad.(List.map (map Proofview.Goal.env) gs) >>= fun envs ->
-        Proofview.tclUNIT (Depends (List.combine envs l))
-
-let lift (type a) (t:a Proofview.tactic) : a t =
-  Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x))
-
-(** If the tactic returns unit, we can focus on the goals if necessary. *)
-let run m k = m >>= function
-| Uniform v -> k v
-| Depends l ->
-  let tacs = List.map k l in
-  Proofview.tclDISPATCH tacs
-
-let (>>=) = bind
-
-let (<*>) = fun m n -> bind m (fun () -> n)
-
-module Self =
-struct
-  type 'a t = 'a focus Proofview.tactic
-  let return = return
-  let (>>=) = bind
-  let (>>) = (<*>)
-  let map f x = x >>= fun a -> return (f a)
-end
-
-module Ftac = Monad.Make(Self)
-module List = Ftac.List
-
-module Notations =
-struct
-  let (>>=) = bind
-  let (<*>) = fun m n -> bind m (fun () -> n)
-end
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
deleted file mode 100644
index 19041f169..000000000
--- a/tactics/ftactic.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Proofview.Notations
-
-(** Potentially focussing tactics *)
-
-type +'a focus
-
-type +'a t = 'a focus Proofview.tactic
-(** The type of focussing tactics. A focussing tactic is like a normal tactic,
-    except that it is able to remember it have entered a goal. Whenever this is
-    the case, each subsequent effect of the tactic is dispatched on the
-    focussed goals. This is a monad. *)
-
-(** {5 Monadic interface} *)
-
-val return : 'a -> 'a t
-(** The unit of the monad. *)
-
-val bind : 'a t -> ('a -> 'b t) -> 'b t
-(** The bind of the monad. *)
-
-(** {5 Operations} *)
-
-val lift : 'a Proofview.tactic -> 'a t
-(** Transform a tactic into a focussing tactic. The resulting tactic is not
-    focussed. *)
-
-val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
-(** Given a continuation producing a tactic, evaluates the focussing tactic. If
-    the tactic has not focussed, then the continuation is evaluated once.
-    Otherwise it is called in each of the currently focussed goals. *)
-
-(** {5 Focussing} *)
-
-val nf_enter : ([ `NF ], 'a t) enter -> 'a t
-(** Enter a goal. The resulting tactic is focussed. *)
-
-val enter : ([ `LZ ], 'a t) enter -> 'a t
-(** Enter a goal, without evar normalization. The resulting tactic is
-    focussed. *)
-
-val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t
-(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *)
-
-val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t
-(** Enter a goal, without evar normalization and put back an evarmap. The
-    resulting tactic is focussed. *)
-
-val with_env : 'a t -> (Environ.env*'a) t
-(** [with_env t] returns, in addition to the return type of [t], an
-    environment, which is the global environment if [t] does not focus on
-    goals, or the local goal environment if [t] focuses on goals. *)
-
-(** {5 Notations} *)
-
-val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
-(** Notation for {!bind}. *)
-
-val (<*>) : unit t -> 'a t -> 'a t
-(** Sequence. *)
-
-(** {5 List operations} *)
-
-module List : Monad.ListS with type 'a t := 'a t
-
-(** {5 Notations} *)
-
-module Notations :
-sig
-  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
-  val (<*>) : unit t -> 'a t -> 'a t
-end
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
deleted file mode 100644
index 008075800..000000000
--- a/tactics/geninterp.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Genarg
-
-module TacStore = Store.Make(struct end)
-
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-module InterpObj =
-struct
-  type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
-  let name = "interp"
-  let default _ = None
-end
-
-module Interp = Register(InterpObj)
-
-let interp = Interp.obj
-let register_interp0 = Interp.register0
-
-let generic_interp ist (GenArg (Glbwit wit, v)) =
-  let open Ftactic.Notations in
-  interp wit ist v >>= fun ans ->
-  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli
deleted file mode 100644
index 0992db7a2..000000000
--- a/tactics/geninterp.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Interpretation functions for generic arguments. *)
-
-open Names
-open Genarg
-
-module TacStore : Store.S
-
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
-
-val generic_interp : (glob_generic_argument, Val.t) interp_fun
-
-val register_interp0 :
-  ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index ab8069225..48722f655 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
 Dnet
 Dn
 Btermdn