aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/indrec.ml
Commit message (Expand)AuthorAge
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Refresh universes in params when generating schemes (Closes: #2429)Gravatar glondu2010-11-08
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* pushed evar reduction in kernelGravatar barras2009-02-06
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...Gravatar notin2006-12-12
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Changement des named_contextGravatar gregoire2005-12-02
* parametres inductifsGravatar mohring2005-11-28
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Eta-expansion du predicat dans build_indrec (suite)Gravatar herbelin2004-07-11
* Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...Gravatar herbelin2004-07-11
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* *** empty log message ***Gravatar barras2003-03-12
* Bug en présence de let-inGravatar herbelin2003-01-15
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14