Normalizing the names of dynamic types to follow a typ_* scheme.

5 files changed, 26 insertions, 26 deletions

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index ffc22f2213..45b0aa2316 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -34,16 +34,16 @@ struct
 
   let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
 
-  let list_tag = ValT.create "list"
-  let opt_tag = ValT.create "option"
-  let pair_tag = ValT.create "pair"
+  let typ_list = ValT.create "list"
+  let typ_opt = ValT.create "option"
+  let typ_pair = ValT.create "pair"
 
   let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
   | Base t -> Dyn (t, x)
-  | List tag -> Dyn (list_tag, List.map (fun x -> inject tag x) x)
-  | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x)
+  | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x)
+  | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x)
   | Pair (tag1, tag2) ->
-    Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x)))
+    Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x)))
 
 end
 
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 5799862110..42e1e3784c 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -31,9 +31,9 @@ sig
   val repr : 'a typ -> string
   val pr : 'a typ -> Pp.std_ppcmds
 
-  val list_tag : t list typ
-  val opt_tag : t option typ
-  val pair_tag : (t * t) typ
+  val typ_list : t list typ
+  val typ_opt : t option typ
+  val typ_pair : (t * t) typ
 
   val inject : 'a tag -> 'a -> t
 
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index a9baef79c7..31bccd019d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -65,7 +65,7 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
 
 let in_list tag v =
   let tag = match tag with Val.Base tag -> tag | _ -> assert false in
-  Val.Dyn (Val.list_tag, List.map (fun x -> Val.Dyn (tag, x)) v)
+  Val.Dyn (Val.typ_list, List.map (fun x -> Val.Dyn (tag, x)) v)
 let in_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
@@ -179,10 +179,10 @@ module Value = struct
   | Some x -> x
 
   let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
-  | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.list_tag v (to_list v))
-  | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.opt_tag v (to_option v))
+  | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
+  | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
   | Val.Pair (tag1, tag2) ->
-    let (x, y) = unbox Val.pair_tag v (to_pair v) in
+    let (x, y) = unbox Val.typ_pair v (to_pair v) in
     (prj tag1 x, prj tag2 y)
   | Val.Base t ->
     let Val.Dyn (t', x) = v in
@@ -1548,19 +1548,19 @@ and interp_genarg ist x : Val.t Ftactic.t =
     | ListArg wit ->
       let map x = interp_genarg ist (Genarg.in_gen (glbwit wit) x) in
       Ftactic.List.map map x >>= fun l ->
-      Ftactic.return (Val.Dyn (Val.list_tag, l))
+      Ftactic.return (Val.Dyn (Val.typ_list, l))
     | OptArg wit ->
       begin match x with
-      | None -> Ftactic.return (Val.Dyn (Val.opt_tag, None))
+      | None -> Ftactic.return (Val.Dyn (Val.typ_opt, None))
       | Some x ->
         interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
-        Ftactic.return (Val.Dyn (Val.opt_tag, Some x))
+        Ftactic.return (Val.Dyn (Val.typ_opt, Some x))
       end
     | PairArg (wit1, wit2) ->
       let (p, q) = x in
       interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
       interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
-      Ftactic.return (Val.Dyn (Val.pair_tag, (p, q)))
+      Ftactic.return (Val.Dyn (Val.typ_pair, (p, q)))
     | ExtraArg s ->
       Geninterp.interp wit ist x
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 6fb68ddf42..9ab6895f3b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -108,12 +108,12 @@ module Make
   | Some Refl -> x
 
   let rec pr_value lev v : std_ppcmds =
-    if has_type v Val.list_tag then
-      pr_sequence (fun x -> pr_value lev x) (unbox v Val.list_tag)
-    else if has_type v Val.opt_tag then
-      pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.opt_tag)
-    else if has_type v Val.pair_tag then
-      let (v1, v2) = unbox v Val.pair_tag in
+    if has_type v Val.typ_list then
+      pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
+    else if has_type v Val.typ_opt then
+      pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
+    else if has_type v Val.typ_pair then
+      let (v1, v2) = unbox v Val.typ_pair in
       str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
     else
       let Val.Dyn (tag, x) = v in
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index a6e7af16e9..d53c1cc04a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -84,11 +84,11 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
-let to_list v = prj Val.list_tag v
+let to_list v = prj Val.typ_list v
 
-let to_option v = prj Val.opt_tag v
+let to_option v = prj Val.typ_opt v
 
-let to_pair v = prj Val.pair_tag v
+let to_pair v = prj Val.typ_pair v
 
 end