diff options
| author | herbelin | 2007-02-13 18:47:49 +0000 |
|---|---|---|
| committer | herbelin | 2007-02-13 18:47:49 +0000 |
| commit | 34ba48a885c91ea895cbba7ba5a53b1ec9de5db8 (patch) | |
| tree | 7c793d76af431bc2cb0aa78e7e9edaa991d1892f /contrib | |
| parent | 6e9c0edd9efc9d72e6f32bc434a34076b1a6afee (diff) | |
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
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 : |