diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 82bb286953..a131c95a54 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -146,7 +146,7 @@ let rec abstract_rawconstr c = function let interp_casted_constr_with_implicits sigma env impls c = (* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) Constrintern.intern_gen false sigma env ~impls:([],impls) - ~allow_soapp:false ~ltacvars:([],[]) c + ~allow_patvar:false ~ltacvars:([],[]) c (* diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index e624b5f329..cab8829dbd 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -53,9 +53,9 @@ let evar_nf isevars c = Evarutil.nf_isevar !isevars c let interp_gen kind isevars env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 846e06cfb4..6de45d17fe 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -14,7 +14,7 @@ val interp_gen : evar_defs ref -> env -> ?impls:full_implicits_env -> - ?allow_soapp:bool -> + ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : |