aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/first-order
Commit message (Expand)AuthorAge
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* firstorder fails gracefullly when encountering untypable higher-order termsGravatar corbinea2006-02-13
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...Gravatar herbelin2005-01-01
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...Gravatar corbinea2004-09-27
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ooops ! bug in firstorder fixed (let's hope no one noticed)Gravatar corbinea2004-03-11
* correction de bugs de congruence et firstorder (inductifs)Gravatar corbinea2004-02-06
* Retablissement de GIntuition juste pour FSetsGravatar herbelin2003-12-23
* *** empty log message ***Gravatar barras2003-12-23
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
* Ground update changing left-arrow-arrow rule.Gravatar corbinea2003-10-13
* Changement de l'afficheur pour que les variables liées aient un nom indépen...Gravatar herbelin2003-09-23
* Passage à la V8 par défautGravatar herbelin2003-09-22
* Ground bugfixGravatar corbinea2003-07-11
* Ground updateGravatar corbinea2003-07-08
* Ground bugfixGravatar corbinea2003-07-04
* switching back to old tautoGravatar corbinea2003-07-03
* modification groundGravatar corbinea2003-07-03
* addition of Auto hints in GroundGravatar corbinea2003-07-03
* added hints into GroundGravatar corbinea2003-07-02
* Ground updateGravatar corbinea2003-06-22
* Ground updateGravatar corbinea2003-06-20
* Ground Update.Gravatar corbinea2003-06-20
* Ground updateGravatar corbinea2003-06-16
* ground updateGravatar corbinea2003-06-16
* Ground major update ... mmm, sounds exciting !Gravatar corbinea2003-06-15
* ground updateGravatar corbinea2003-06-14
* Major Ground update, may break semanticsGravatar corbinea2003-06-14
* Ground updateGravatar corbinea2003-06-13
* Ground update, new files.Gravatar corbinea2003-06-13
* Ground update.Gravatar corbinea2003-06-13
* Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...Gravatar herbelin2003-06-10
* bugfix for Ground ( merci JC )Gravatar corbinea2003-06-04
* Ground update + some bugfixGravatar corbinea2003-06-04
* Ground daily updateGravatar corbinea2003-05-29