aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/TreeMod/ZTreeMod.v
diff options
context:
space:
mode:
authorherbelin2008-04-27 16:15:34 +0000
committerherbelin2008-04-27 16:15:34 +0000
commitecf68d1ed251e2c6b4abd9e97400d3ab009d2925 (patch)
tree816959daf3aa5d5b7469ecc7c4bcc72e517aed76 /theories/Numbers/Integer/TreeMod/ZTreeMod.v
parente961ace331ec961dcec0e2525d7b9142d04b5154 (diff)
- Backtrack sur option with_types suite à confusion sur l'utilisation
des types des with-bindings dans la 8.1 [ceux-ci étaient déjà utilisés et ce qui est vraiment nouveau est que l'unification est maintenant celle de evarconv alors que c'était avant un mélange d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je renonce à maintenir la compatibilité (on se retrouve donc avec un exemple qui fonctionne différement dans TermsConv.v de CoLoR). - Robustesse accrue pour la nouvelle facilité de syntaxe de binding avec paramètre pour pose/set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/TreeMod/ZTreeMod.v')
0 files changed, 0 insertions, 0 deletions