aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.ml
Commit message (Expand)AuthorAge
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Changement des named_contextGravatar gregoire2005-12-02
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Set is not always impredicativeGravatar barras2004-01-12
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* un cas inutile dans un pattern matchingGravatar letouzey2002-07-16
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* exceptionmal ratrappeeGravatar barras2002-02-04
* Grossière erreur de typageGravatar herbelin2001-12-18
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Blindage, de peur que des types entrant non en forme normale ne provoque des ...Gravatar herbelin2001-09-19
* Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...Gravatar herbelin2001-09-19
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Bug env vis à vis du let inGravatar herbelin2000-12-15
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* 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
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Achèvement abstraction du mécanisme (optionnel) de castGravatar herbelin2000-06-29
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* RéorganisationGravatar herbelin2000-05-05
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...Gravatar herbelin2000-03-21
* MAJ nouveau try_mutind_ofGravatar herbelin2000-03-08
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 15:57:49 +0000