aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorletouzey2006-05-11 09:38:28 +0000
committerletouzey2006-05-11 09:38:28 +0000
commitfc5dcb9e0dac748bfb40a1523d0811490158cada (patch)
tree5cb47cb090fdc27b74419ec2a480a97b8ec105d8 /kernel/inductive.ml
parent0fb3feddf3e70b4b492129eec68837a5c84bf50c (diff)
Duplication du fichier FSetProperties pour les ensembles Weak.
Du coup, factorisation d'une partie dans SetoidList. Ajout de lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface concernant elements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions