aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega
Commit message (Expand)AuthorAge
* Mise en conformité nouveau Simpl pour FixGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Opaque pas encore implementee; syntax langage tactiquesGravatar filliatr2000-07-03
* Auto with zarith provisoirement remplace par un OmegaGravatar filliatr2000-06-12
* un Declare ML Module inutileGravatar filliatr2000-05-08
* retour a la version qui ne contournait pas le bug de PatternMatchingFailure n...Gravatar herbelin2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
* MODIFS pour compatibilité aussi 2.99Gravatar herbelin2000-04-30
* mise sous CVS d'OmegaGravatar filliatr2000-04-28