aboutsummaryrefslogtreecommitdiff
path: root/toplevel/recordobj.ml
AgeCommit message (Expand)Author
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2003-03-12*** empty log message ***barras
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-05GROS COMMIT:barras
2001-10-16Nettoyage Recordobj et conséquencesherbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-03-15entetesfilliatr
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-01-30Les Objdef introduisent une convertibilité avec les projections dans le test...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:37:06 +0000