diff options
| author | bertot | 2006-08-17 13:42:36 +0000 |
|---|---|---|
| committer | bertot | 2006-08-17 13:42:36 +0000 |
| commit | c7446212657af6c407b95736b4fe13c6e26d5690 (patch) | |
| tree | 913740b690073241448511b4b6af0a29d23442c4 /doc/RecTutorial/RecTutorial.v | |
| parent | fc37b6ea9f7cfb26e62b5cb95973f1a9ab52284a (diff) | |
corrects an error in the substitution of module paths inside tactics:
objects of the form TacDynamic should not be left unchanged if their content
is tagged with "constr". This correction makes that setoid ring can
now work with rings that were declared inside a module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RecTutorial/RecTutorial.v')
0 files changed, 0 insertions, 0 deletions