diff options
| author | herbelin | 2008-07-24 08:22:17 +0000 |
|---|---|---|
| committer | herbelin | 2008-07-24 08:22:17 +0000 |
| commit | 80921b2f279b70f60cb66684f88c7e6f180f8117 (patch) | |
| tree | f65c6ea2c388e2e3c7df5f041ab4b28c9078737a /doc/RecTutorial | |
| parent | 16084065ebcff9eeba7231e687611fd9acb54887 (diff) | |
Propagation de l'information "strict" (càd à toplevel ou en train de
définir une ltac) dans l'interprétation des identificateurs isolés en
position de tactiques, comme dans "let x:=y in t" (résoud
l'incompatibilité #1906).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions