diff options
| author | herbelin | 2006-10-05 07:45:01 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-05 07:45:01 +0000 |
| commit | 4df304ac6f2c6e5de3d0976d3e866ee457bb38df (patch) | |
| tree | 7194d7577f7dcab000baca57e421fca036d52f0b /interp/topconstr.ml | |
| parent | d2204d89037471c265ab70afb9f03983869948db (diff) | |
Essai de changement de sémantique du %scope :
1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer
récursivement pour toutes les notations de l'expression concernée;
2- désactive la pile de scope pour cette notation immédiate.
Le point 2 est clairement préférable pour les notations de la forme
3%sc, où on ne veut pas que 3 soit interprété dans un autre scope
que sc même si sc n'a pas de notations numériques. Le point 1 est plus
discutable et risque aussi de poser des incompatibilité (mais le
comportement récursif peut être rétabli en changeant la valeur de
quelques booléens marqués "recursive" dans constrextern.ml,
constrintern.ml, et notation.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9208 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c613bf0dbe..c9ae593afd 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -480,8 +480,12 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) = type scope_name = string +type tmp_scope_name = + | LightTmpScope of scope_name + | ExplicitTmpScope of scope_name + type interpretation = - (identifier * (scope_name option * scope_name list)) list * aconstr + (identifier * (tmp_scope_name option * scope_name list)) list * aconstr let match_aconstr c (metas_scl,pat) = let subst = match_ [] (List.map fst metas_scl) [] c pat in |