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