diff options
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 5fa781ad..e6d9f99d 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: argextend.ml4,v 1.9.2.2 2004/07/16 19:30:37 herbelin Exp $ *) +(* $Id: argextend.ml4,v 1.9.2.4 2005/01/15 14:56:53 herbelin Exp $ *) open Genarg open Q_util @@ -33,6 +33,7 @@ let rec make_rawwit loc = function | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | TacticArgType -> <:expr< Genarg.rawwit_tactic >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> + | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >> | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> @@ -59,6 +60,7 @@ let rec make_globwit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.globwit_tactic >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> + | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >> | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> @@ -85,6 +87,7 @@ let rec make_wit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.wit_tactic >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> + | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >> | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> @@ -267,11 +270,14 @@ EXTEND declare_vernac_argument false loc s l ] ] ; argtype: - [ [ e = LIDENT -> fst (interp_entry_name loc e) - | e1 = LIDENT; "*"; e2 = LIDENT -> - let e1 = fst (interp_entry_name loc e1) in - let e2 = fst (interp_entry_name loc e2) in - PairArgType (e1, e2) ] ] + [ "2" RIGHTA + [ e1 = argtype; "*"; e2 = NEXT -> PairArgType (e1, e2) ] + | "1" + [ e = argtype; LIDENT "list" -> List0ArgType e + | e = argtype; LIDENT "option" -> OptArgType e ] + | "0" + [ e = LIDENT -> fst (interp_entry_name loc e) + | "("; e = argtype; ")" -> e ] ] ; argrule: [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] @@ -286,4 +292,3 @@ EXTEND ] ] ; END - |