aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.mli
Commit message (Expand)AuthorAge
...
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Ajout alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* find_section_variable : un traducteur id -> sp pour variables de section; var...Gravatar herbelin2000-12-25
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* NettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametab + nettoyageGravatar herbelin2000-11-26
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Nouveaux points d'accès pour les noms qualifiésGravatar herbelin2000-11-20
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* Renommage canonique :Gravatar herbelin2000-10-18
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* portage Omega (code seulement)Gravatar filliatr2000-04-28
* discharge des axiomesGravatar filliatr2000-04-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* modulesGravatar filliatr1999-12-12
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* - global_reference traite des variablesGravatar filliatr1999-12-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* Pfedit (fin)Gravatar filliatr1999-12-02
* poursuite de VernacentriesGravatar filliatr1999-12-01
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* make_strength / reset_libraryGravatar filliatr1999-12-01
* portage Astterm (partiellement)Gravatar filliatr1999-11-29
* module Classops; ajout de fonctions dans Declare en consequenceGravatar filliatr1999-11-26
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* module DeclareGravatar filliatr1999-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 13:17:52 +0000