aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega/coq_omega.ml
Commit message (Expand)AuthorAge
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* id_of_global devient sp_of_globalGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Nettoyage Names suiteGravatar herbelin2000-11-07
* 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
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* MODIFS pour compatibilité aussi 2.99Gravatar herbelin2000-04-30
* mise sous CVS d'OmegaGravatar filliatr2000-04-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 14:14:11 +0000