diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a8dad2216a..357ce43774 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1277,8 +1277,9 @@ let interp_constr_judgment_evars evdref env c = type ltac_sign = identifier list * unbound_ltac_var_map -let interp_constrpattern sigma env c = - pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c) +let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = + let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in + pattern_of_rawconstr c let interp_aconstr impls (vars,varslist) a = let env = Global.env () in |