Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Renommage AppL en App | herbelin | 2000-10-01 |
* | Disparition du type oper mais nouveau type global_reference | herbelin | 2000-10-01 |
* | Abstraction de constr | herbelin | 2000-09-14 |
* | Modification mkAppL; abstraction via kind_of_term; changement dans Reduction | herbelin | 2000-09-12 |
* | Ajout d'un LetIn primitif. | herbelin | 2000-09-10 |
* | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin | 2000-07-24 |
* | Opaque pas encore implementee; syntax langage tactiques | filliatr | 2000-07-03 |
* | Auto with zarith provisoirement remplace par un Omega | filliatr | 2000-06-12 |
* | un Declare ML Module inutile | filliatr | 2000-05-08 |
* | retour a la version qui ne contournait pas le bug de PatternMatchingFailure n... | herbelin | 2000-05-03 |
* | Ajout du langage de tactiques | delahaye | 2000-05-03 |
* | portage Omega (mais toujours pas Zpower et Zlogarithm) | filliatr | 2000-05-02 |
* | MODIFS pour compatibilité aussi 2.99 | herbelin | 2000-04-30 |
* | mise sous CVS d'Omega | filliatr | 2000-04-28 |