aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.mli
Commit message (Expand)AuthorAge
...
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Nouvelle en-têteGravatar herbelin2004-07-16
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* MAJ pour make docGravatar herbelin2001-11-09
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* nettoyage extractionGravatar filliatr2001-05-09
* entetesGravatar filliatr2001-03-15
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* make docGravatar herbelin2001-01-27
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Correction pb de globalisation dans print_mutualGravatar herbelin2000-10-18
* Renommage des find_m*typeGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* docGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Ajout mis_typepathGravatar herbelin2000-05-16
* Retrait fullmind de inductive_summary pour simplicitéGravatar herbelin2000-04-27
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et...Gravatar herbelin2000-03-21
* Peaufinement nouveaux types inductive_summary et constructor_summary en vueGravatar herbelin2000-03-08
* documentationGravatar filliatr2000-01-28
* erreurs latex dans interfacesGravatar filliatr2000-01-27
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* explicitations erreurs inductifsGravatar filliatr1999-12-05
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* module WcclausenvGravatar filliatr1999-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:54:11 +0000