aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-08-30Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Serverherbelin
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-08-24Utilisation plus précise de la contrainte de type pour interpréter lesherbelin
2007-08-20Modification de l'initialisation des chemins de la librairie standardnotin
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
2007-05-17Nettoyage et standardisation des messages d'erreurs.herbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Multiples changements autour des implicites :herbelin
2007-04-29Correction bug #1507 (report révision 9807 de v8.1 vers trunk)herbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-04-17Reorder hook and printing of message, more natural this way.msozeau
2007-04-17 Added the option to set/unset the automatic generation of elimination schemesvsiles
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
2007-02-21Utilisation de l'environnement pour l'affichage de certains messages d'erreursherbelin
2007-02-07Vérification que toutes les evars ont étés instanciées dans les types imp...herbelin
2007-01-24Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentherbelin
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-12-28Cleaning backtracking code, optimized "Backtrack n x y" when n iscourtieu
2006-12-23Addition of a "Combined Scheme" vernacular command for building the conjuncti...msozeau
2006-12-12Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...notin
2006-12-08Suite ajout option -output-contextherbelin
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
2006-11-24Fixed the -emacs option which was always On.courtieu
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
2006-11-02gestion speciale du niveau 5 des ltacbarras
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-28Documentation de "Set Printing Universes", "Print Universes" (anciennementherbelin
2006-10-28Ajout option Set Printing Universes et amélioration affichage des universherbelin
2006-10-23bug #1194: normalisation evars a la sortie de focusbarras
2006-10-23Add a flush after backtracking x y z and before printing subgoals.courtieu
2006-10-20Correction de la localisation des erreurs en interactif (numéro deherbelin
2006-10-09Amélioration de l'automatisation des coupures quand deux idents se suiventherbelin
2006-10-05Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...notin