aboutsummaryrefslogtreecommitdiff
path: root/doc/RecTutorial
diff options
context:
space:
mode:
authorbertot2006-08-17 13:42:36 +0000
committerbertot2006-08-17 13:42:36 +0000
commitc7446212657af6c407b95736b4fe13c6e26d5690 (patch)
tree913740b690073241448511b4b6af0a29d23442c4 /doc/RecTutorial
parentfc37b6ea9f7cfb26e62b5cb95973f1a9ab52284a (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')
0 files changed, 0 insertions, 0 deletions