diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index a646b6314..6410c9b2e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -113,8 +113,9 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment (* Interprets constr patterns *) -val interp_constrpattern : - evar_map -> env -> constr_expr -> patvar list * constr_pattern +val intern_constr_pattern : + evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + constr_pattern_expr -> patvar list * constr_pattern val interp_reference : ltac_sign -> reference -> rawconstr |