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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 799361a27d..1bbf87a40b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -536,7 +536,7 @@ let intern_hyp_location ist ((occs,id),hl) = ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl) let interp_constrpattern_gen sigma env ltacvar c = - let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[]) + let c = intern_gen false ~allow_patvar:true ~ltacvars:(ltacvar,[]) sigma env c in pattern_of_rawconstr c |