aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness
Commit message (Collapse)AuthorAge
...
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation d'un bug de Correctness: whd_programs ne doit pas réduire les ↵Gravatar filliatr2001-04-11
| | | | | | terms contenant des Evar pas des Metas; mise à jour des exemples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegaGravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1573 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
* exemples CorrectnessGravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵Gravatar filliatr2001-04-04
| | | | | | d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
* deux fichiers (past et ptype) uniquement sous forme de .mliGravatar filliatr2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1527 85f007b7-540e-0410-9357-904b9bb8a0f7
* psyntax.ml4 sous CVSGravatar filliatr2001-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1520 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness (ne compile pas encore)Gravatar filliatr2001-03-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7