aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Fix wrong environment bug in test for setoid_rewrite or rewrite.Gravatar msozeau2008-07-28
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Show configure choice for browser in CoqIDE preferencesGravatar glondu2008-07-28
* Now, -browser option is effective (and compiles)Gravatar glondu2008-07-27
* (Partially) Revert previous commit because of FTBFSGravatar glondu2008-07-27
* Add -browser option to configure scriptGravatar glondu2008-07-27
* Oups (on refait le 11268 en mieux)Gravatar herbelin2008-07-27
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
* Suite 11266 (warning tools/gallina.ml)Gravatar herbelin2008-07-25
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Fixed bug #1904 (instances of evars were no longer substituted sinceGravatar herbelin2008-07-25
* A better test for relations being setoids or not: do leibniz rewrite iffGravatar msozeau2008-07-25
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* A (safe) implementation of prolog's cut in the typeclasses eauto to avoidGravatar msozeau2008-07-24
* Fix bug #1913, checking for unresolved evars which aren't obligations.Gravatar msozeau2008-07-24
* fixed loop in dependency fold of the checkerGravatar barras2008-07-24
* moved magic numbers to configure (share coq/coqchk)Gravatar barras2008-07-24
* broke cyclic dependenciesGravatar barras2008-07-24
* Suite commit 11236Gravatar notin2008-07-24
* Propagation de l'information "strict" (càd à toplevel ou en train deGravatar herbelin2008-07-24
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Oops... forgot some debug code.Gravatar msozeau2008-07-23
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Oubli lors du commit #11236Gravatar notin2008-07-22
* Suite commit 11236Gravatar notin2008-07-21
* Extraction: better dependency computation (after optimisations)Gravatar letouzey2008-07-20
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Affichage intempestif d'information de globalisation + numéro de version dan...Gravatar notin2008-07-18
* fixed indentation of subgoals for Show ScriptGravatar barras2008-07-17
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
* - coqdoc: correction d'un bug sur les commentaires imbriquésGravatar notin2008-07-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, re...Gravatar notin2008-07-16
* ROmega : make it work even if no Require Import ZArith has been doneGravatar letouzey2008-07-16
* Ajout d'une option pour contrôler l'installation automatique de la documenta...Gravatar notin2008-07-16
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* Autour du parsing:Gravatar herbelin2008-07-15
* Tentative de relecture des scripts de Mult.v au regard des tactiques actuellesGravatar herbelin2008-07-15
* update doc MicromegaGravatar fbesson2008-07-13
* Correction d'un autre bug autour de la gestion des niveaux vides deGravatar herbelin2008-07-11
* Bug résiduel du backtrack de coqide se produisant lorsque la limite deGravatar herbelin2008-07-10