Interpretation function can return any untyped value.

5 files changed, 36 insertions, 29 deletions

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index a3e494f5c..ffc22f221 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -86,16 +86,13 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
 module InterpObj =
 struct
-  type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
+  type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun
   let name = "interp"
   let default _ = None
 end
 
 module Interp = Register(InterpObj)
 
-let interp wit ist v =
-  let f = Interp.obj wit in
-  let tag = val_tag (Topwit wit) in
-  Ftactic.bind (f ist v) (fun v -> Ftactic.return (Val.inject tag v))
+let interp = Interp.obj
 
 let register_interp0 = Interp.register0
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index c92181027..579986211 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -64,4 +64,4 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun
 
 val register_interp0 :
-  ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
+  ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 2618e5d89..3b7e180c6 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -119,19 +119,21 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
   let interp = match f with
     | None ->
       begin match globtyp with
-      | None -> <:expr< fun ist v -> Ftactic.return v >>
+      | None ->
+        let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
+        <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >>
       | Some globtyp ->
         <:expr< fun ist x ->
-          Ftactic.bind
-            (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
-            (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
+          Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >>
       end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
+      let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
       <:expr<
         let f = $lid:f$ in
         fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl ->
           let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
+          let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in
           Sigma.Unsafe.of_pair (Ftactic.return v, sigma)
         }
       >> in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index a3e6e0ebe..94c13a0e0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -2042,6 +2042,13 @@ let hide_interp global t ot =
 (***************************************************************************)
 (** Register standard arguments *)
 
+let register_interp0 wit f =
+  let open Ftactic.Notations in
+  let interp ist v =
+    f ist v >>= fun v -> Ftactic.return (Val.inject (val_tag wit) v)
+  in
+  Geninterp.register_interp0 wit interp
+
 let def_intern ist x = (ist, x)
 let def_subst _ x = x
 let def_interp ist x = Ftactic.return x
@@ -2049,7 +2056,7 @@ let def_interp ist x = Ftactic.return x
 let declare_uniform t =
   Genintern.register_intern0 t def_intern;
   Genintern.register_subst0 t def_subst;
-  Geninterp.register_interp0 t def_interp
+  register_interp0 t def_interp
 
 let () =
   declare_uniform wit_unit
@@ -2090,33 +2097,33 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   }
 
 let () =
-  Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
-  Geninterp.register_interp0 wit_ref (lift interp_reference);
-  Geninterp.register_interp0 wit_ident (lift interp_ident);
-  Geninterp.register_interp0 wit_var (lift interp_hyp);
-  Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
-  Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
-  Geninterp.register_interp0 wit_constr (lifts interp_constr);
-  Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
-  Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
-  Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
-  Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
-  Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr);
-  Geninterp.register_interp0 wit_bindings interp_bindings';
-  Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
-  Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
+  register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+  register_interp0 wit_ref (lift interp_reference);
+  register_interp0 wit_ident (lift interp_ident);
+  register_interp0 wit_var (lift interp_hyp);
+  register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
+  register_interp0 wit_clause_dft_concl (lift interp_clause);
+  register_interp0 wit_constr (lifts interp_constr);
+  register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
+  register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
+  register_interp0 wit_red_expr (lifts interp_red_expr);
+  register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
+  register_interp0 wit_open_constr (lifts interp_open_constr);
+  register_interp0 wit_bindings interp_bindings';
+  register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
+  register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
   ()
 
 let () =
   let interp ist tac = Ftactic.return (Value.of_closure ist tac) in
-  Geninterp.register_interp0 wit_tactic interp
+  register_interp0 wit_tactic interp
 
 let () =
   let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
-  Geninterp.register_interp0 wit_ltac interp
+  register_interp0 wit_ltac interp
 
 let () =
-  Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
+  register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
   end })
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1c..b04c4a50c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
 ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw