aboutsummaryrefslogtreecommitdiff
path: root/contrib/first-order
AgeCommit message (Expand)Author
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-02-22Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...notin
2007-01-28"suffices" implemented + syntax cleanupcorbinea
2006-09-20Declarative Proof Language: main commitcorbinea
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-02-13firstorder fails gracefullly when encountering untypable higher-order termscorbinea
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ...herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-02Types inductifs parametriquesmohring
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-01Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...herbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-09-27firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...corbinea
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-07-16Nouvelle en-têteherbelin
2004-03-11Ooops ! bug in firstorder fixed (let's hope no one noticed)corbinea
2004-02-06correction de bugs de congruence et firstorder (inductifs)corbinea
2003-12-23Retablissement de GIntuition juste pour FSetsherbelin
2003-12-23*** empty log message ***barras
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-13factorisation et generalisation des clausesbarras
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-10-13Ground update changing left-arrow-arrow rule.corbinea
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-22Passage à la V8 par défautherbelin
2003-07-11Ground bugfixcorbinea
2003-07-08Ground updatecorbinea
2003-07-04Ground bugfixcorbinea
2003-07-03switching back to old tautocorbinea
2003-07-03modification groundcorbinea
2003-07-03addition of Auto hints in Groundcorbinea
2003-07-02added hints into Groundcorbinea
2003-06-22Ground updatecorbinea
2003-06-20Ground updatecorbinea
2003-06-20Ground Update.corbinea