From de4b9b68445d9f3e48da789404cbdfcd89214585 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 18 Apr 2016 14:39:34 +0200
Subject: Moving the Val module to Geninterp.

---
 grammar/argextend.ml4 | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dca3e1656..2618e5d89 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -88,6 +88,7 @@ let check_type prefix s = function
 | Some _ -> warning_redundant prefix s
 
 let declare_tactic_argument loc s (typ, f, g, h) cl =
+  let se = mlexpr_of_string s in
   let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with
     | `Uniform (typ, pr) ->
       let typ = get_type "" s typ in
@@ -147,20 +148,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
   | None -> <:expr< None >>
-  | Some typ ->
-    if is_self s typ then <:expr< None >>
-    else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
+  | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >>
   in
-  let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   declare_str_items loc
-   [ <:str_item<
-      value ($lid:"wit_"^s$) =
-        let dyn = $dyn$ in
-        Genarg.make0 ?dyn $se$ >>;
+   [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>;
      <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
      <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
      <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
+     <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>;
      make_extend loc s cl wit;
      <:str_item< do {
       Pptactic.declare_extra_genarg_pprule
-- 
cgit v1.2.3