Switching to an untyped toplevel representation for Ltac values.

3 files changed, 17 insertions, 16 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc6ff03b4b..d7ce0d4c1a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,7 +156,7 @@ 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 = Val.inject (val_tag (topwit Constrarg.wit_constr)) c 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
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 358f6d6468..298257e45d 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -24,13 +24,18 @@ let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
   Genarg.create_arg "constr_under_binders"
 
+(** 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
   match Val.eq t (val_tag wit) with
   | 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 +79,17 @@ 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 to_list v = prj Val.list_tag v
 
-let of_list t v = Val.Dyn (Val.List t, v)
+let of_list t v = Val.Dyn (Val.list_tag, List.map (fun v -> Val.inject t v) 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.opt_tag v
+
+let of_option t v = Val.Dyn (Val.opt_tag, Option.map (fun v -> Val.inject t v) v)
+
+let to_pair v = prj Val.pair_tag v
 
-let of_option t v = Val.Dyn (Val.Opt t, v)
+let of_pair t1 t2 (v1, v2) = Val.Dyn (Val.pair_tag, (Val.inject t1 v1, Val.inject t2 v2))
 
 end
 
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 87137fd2e7..75a3b347d6 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -44,6 +44,8 @@ sig
   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
+  val of_pair : 'a Val.tag -> 'b Val.tag -> ('a * 'b) -> t
 end
 
 (** {5 Coercion functions} *)