From 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Dec 2015 18:04:14 +0100
Subject: Removing ad-hoc interpretation rules for tactic notations and their
 genarg.

Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
---
 grammar/argextend.ml4 | 2 --
 grammar/q_coqast.ml4  | 2 --
 2 files changed, 4 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 842f59809f..b9336ce333 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -30,11 +30,9 @@ let mk_extraarg loc s =
     <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
-  | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
   | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
   | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3088e03654..7001f5f627 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -223,12 +223,10 @@ let mlexpr_of_red_expr = function
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
-  | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
-  | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.PairArgType (t1,t2) ->
-- 
cgit v1.2.3