aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-03-17 04:57:32 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-03-17 04:57:32 +0000
commit1a750105e7d9630acf44dd0833cdc34578a0aea5 (patch)
tree5165a4abf83dec76bca5fc37fdc1403e23c0bb58 /theories/Reals
parent6e616fea2b9e153b04232537b7ee2539409521ac (diff)
Meilleure gestion de la reduction dans Field
Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions