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.

2 files changed, 4 insertions, 101 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index ef0de89afb..69408fb1a5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,7 +9,6 @@
 open Pp
 open Util
 
-module ValT = Dyn.Make(struct end)
 module ArgT =
 struct
   module DYN = Dyn.Make(struct end)
@@ -25,52 +24,6 @@ struct
     Some (Any (Obj.magic t)) (** All created tags are made of triples *)
 end
 
-module Val =
-struct
-
-  type 'a typ = 'a ValT.tag
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a tag * 'a -> t
-
-  let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option =
-  fun t1 t2 -> match t1, t2 with
-  | Base t1, Base t2 -> ValT.eq t1 t2
-  | List t1, List t2 ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl -> Some Refl
-    end
-  | Opt t1, Opt t2 ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl -> Some Refl
-    end
-  | Pair (t1, u1), Pair (t2, u2) ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl ->
-      match eq u1 u2 with
-      | None -> None
-      | Some Refl -> Some Refl
-    end
-  | _ -> None
-
-  let repr = ValT.repr
-
-  let rec pr : type a. a tag -> std_ppcmds = function
-  | Base t -> str (repr t)
-  | List t -> pr t ++ spc () ++ str "list"
-  | Opt t -> pr t ++ spc () ++ str "option"
-  | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")"
-
-end
-
 type (_, _, _) genarg_type =
 | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
 | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
@@ -202,36 +155,14 @@ struct
   include ArgT.Map(struct type 'a t = 'a pack end)
 end
 
-type ('raw, 'glb, 'top) load = {
-  dyn : 'top Val.tag;
-}
-
-module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
-
-let arg0_map = ref LoadMap.empty
-
-let create_arg ?dyn name =
+let create_arg name =
   match ArgT.name name with
+  | None -> ExtraArg (ArgT.create name)
   | Some _ ->
     Errors.anomaly (str "generic argument already declared: " ++ str name)
-  | None ->
-    let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
-    let obj = LoadMap.Pack { dyn; } in
-    let name = ArgT.create name in
-    let () = arg0_map := LoadMap.add name obj !arg0_map in
-    ExtraArg name
 
 let make0 = create_arg
 
-let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
-| ListArg t -> Val.List (val_tag t)
-| OptArg t -> Val.Opt (val_tag t)
-| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
-| ExtraArg s ->
-  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn
-
-let val_tag = function Topwit t -> val_tag t
-
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 93665fd45d..b8bb6af04a 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -86,36 +86,14 @@ type (_, _, _) genarg_type =
 (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
     one, and ['top] the internalized one. *)
 
-module Val :
-sig
-  type 'a typ
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a tag * 'a -> t
-
-  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-  val repr : 'a typ -> string
-  val pr : 'a tag -> Pp.std_ppcmds
-
-end
-(** Dynamic types for toplevel values. While the generic types permit to relate
-    objects at various levels of interpretation, toplevel values are wearing
-    their own type regardless of where they came from. This allows to use the
-    same runtime representation for several generic types. *)
-
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -180,12 +158,6 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
-(** {6 Dynamic toplevel values} *)
-
-val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
-(** Retrieve the dynamic type associated to a toplevel genarg. Only works for
-    ground generic arguments. *)
-
 (** {6 Type reification} *)
 
 type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type