diff options
| author | Julien Forest | 2014-04-14 23:22:14 +0200 |
|---|---|---|
| committer | Julien Forest | 2014-04-14 23:22:14 +0200 |
| commit | 5fb2050e424062540ffbf22de0838fafe4de0a41 (patch) | |
| tree | 235a18a0481828d9af31c28df41e3492c5adb044 /interp | |
| parent | a51d94e77bd352522744da4dbdbf98b36c19631e (diff) | |
Closing bug #3260
adding a new grammar entry for clauses
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 4 | ||||
| -rw-r--r-- | interp/constrarg.mli | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 37e627a6d4..c25e02c02c 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -55,6 +55,9 @@ let wit_bindings = unsafe_of_type BindingsArgType let wit_red_expr = unsafe_of_type RedExprArgType +let wit_clause_dft_concl = + Genarg.make0 None "clause_dft_concl" + (** Register location *) let () = @@ -62,3 +65,4 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 5faef378a6..d5d19f2eaa 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -30,6 +30,7 @@ val wit_int_or_var : int or_var uniform_genarg_type val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type + val wit_ident : Id.t uniform_genarg_type val wit_var : (Id.t located, Id.t located, Id.t) genarg_type @@ -68,3 +69,5 @@ val wit_red_expr : (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type + +val wit_clause_dft_concl : (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type |