diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index ef7cdbfa3a..10afcdd21a 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -15,7 +15,6 @@ open Pp open Names open Genarg open Q_util -open Q_coqast open Argextend open Pcoq open Egramml @@ -32,6 +31,15 @@ let rec make_patt = function <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l +let rec mlexpr_of_argtype loc = function + | 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) -> + let t1 = mlexpr_of_argtype loc t1 in + let t2 = mlexpr_of_argtype loc t2 in + <:expr< Genarg.PairArgType $t1$ $t2$ >> + | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> + let rec make_when loc = function | [] -> <:expr< True >> | ExtNonTerminal (t, _, p) :: l -> |