aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/ring.ml
Commit message (Expand)AuthorAge
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* 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
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'Gravatar herbelin2000-10-26
* Manquait le cas Constr de dyn_polynomGravatar herbelin2000-10-25
* 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
* Suppression de AbstGravatar herbelin2000-09-10
* RingGravatar filliatr2000-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-30 02:23:32 +0000