Change the toplevel representation of Ltac values to an untyped one.

This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.

This is mostly an API change, as it did not break any contrib outside of mathcomp.

9 files changed, 27 insertions, 273 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc6ff03b4b..6b58baa997 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,11 +156,16 @@ let conclPattern concl pat tac =
        constr_bindings env sigma >>= fun constr_bindings ->
      let open Genarg in
      let open Geninterp in
-     let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+     let inj c = match val_tag (topwit Constrarg.wit_constr) with
+     | Val.Base tag -> Val.Dyn (tag, c)
+     | _ -> assert false
+     in
      let fold id c accu = Id.Map.add id (inj c) accu in
      let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
      let ist = { lfun; extra = TacStore.empty } in
-     Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+     match tac with
+     | GenArg (Glbwit wit, tac) ->
+      Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
   end }
 
 (***********************************************************)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4816f8a452..950eeef520 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -106,9 +106,9 @@ let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = List.map (fun h -> 
   let tac = match h.rew_tac with
   | None -> Proofview.tclUNIT ()
-  | Some tac ->
+  | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
-    Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+    Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
   in
     (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
     Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
deleted file mode 100644
index 588709873e..0000000000
--- 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 19041f1698..0000000000
--- 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 0080758000..0000000000
--- 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 0992db7a29..0000000000
--- 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/taccoerce.ml b/tactics/taccoerce.ml
index 358f6d6468..d53c1cc04a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,15 +14,25 @@ open Misctypes
 open Genarg
 open Stdarg
 open Constrarg
+open Geninterp
 
 exception CannotCoerceTo of string
 
 let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
-  Genarg.create_arg "constr_context"
+  let wit = Genarg.create_arg "constr_context" in
+  let () = register_val0 wit None in
+  wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
-  Genarg.create_arg "constr_under_binders"
+  let wit = Genarg.create_arg "constr_under_binders" in
+  let () = register_val0 wit None in
+  wit
+
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
@@ -30,7 +40,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w
   | None -> false
   | Some Refl -> true
 
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   let Val.Dyn (t', x) = v in
   match Val.eq t t' with
   | None -> None
@@ -74,23 +84,11 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
-let to_list v =
-  let v = normalize v in
-  let Val.Dyn (tag, v) = v in
-  match tag with
-  | Val.List t -> Some (List.map (fun x -> Val.Dyn (t, x)) v)
-  | _ -> None
-
-let of_list t v = Val.Dyn (Val.List t, v)
+let to_list v = prj Val.typ_list v
 
-let to_option v =
-  let v = normalize v in
-  let Val.Dyn (tag, v) = v in
-  match tag with
-  | Val.Opt t -> Some (Option.map (fun x -> Val.Dyn (t, x)) v)
-  | _ -> None
+let to_option v = prj Val.typ_opt v
 
-let of_option t v = Val.Dyn (Val.Opt t, v)
+let to_pair v = prj Val.typ_pair v
 
 end
 
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 87137fd2e7..7a963f95f3 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -12,6 +12,7 @@ open Term
 open Misctypes
 open Pattern
 open Genarg
+open Geninterp
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
@@ -41,9 +42,8 @@ sig
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
-  val of_list : 'a Val.tag -> 'a list -> t
   val to_option : t -> t option option
-  val of_option : 'a Val.tag -> 'a option -> t
+  val to_pair : t -> (t * t) option
 end
 
 (** {5 Coercion functions} *)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index ab8069225d..48722f655a 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
 Dnet
 Dn
 Btermdn