aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Suite révision 10495Gravatar herbelin2008-02-01
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Fix obvious syntax error. Forgot to recompile before commiting...Gravatar msozeau2008-01-31
* Remove unneeded .d mask, can be set localy by each dev inGravatar msozeau2008-01-31
* Ignore generated dependency files.Gravatar msozeau2008-01-31
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Finish let| implementation and document itGravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Support for occurences and 'in' in class_setoid, work on corresponding tactic...Gravatar msozeau2008-01-30
* Use new redefinition support for the default obligations tacticGravatar msozeau2008-01-30
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
* Add occurence extra argGravatar msozeau2008-01-30
* Debug 0-ary typeclasses support, use new redefinition support for default tacticGravatar msozeau2008-01-30
* Add list_iter3 Gravatar msozeau2008-01-30
* Add some keywordGravatar msozeau2008-01-30
* Added full documentation for mathematical mode (draft version)Gravatar corbinea2008-01-29
* Correction du bug #1785Gravatar notin2008-01-29
* Nicer proofs.Gravatar roconnor2008-01-24
* remove Fourier Failure warnings.Gravatar roconnor2008-01-24
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24
* Fermeture du bug #1754Gravatar notin2008-01-24
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* Changing R to a local definition so that it isn't exported.Gravatar roconnor2008-01-23
* Ajout d'un test pour le bug #1779Gravatar notin2008-01-23
* Ajout d'un test pour le mode déclaratif + test pour le bug #1776Gravatar notin2008-01-23
* TypoGravatar notin2008-01-23
* Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)Gravatar notin2008-01-22
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* Récupération d'une exception Not_foundGravatar notin2008-01-22
* Correction du bug #1754Gravatar notin2008-01-21
* cosmetics: after an extract inductive to bool, let's use if then elseGravatar letouzey2008-01-20
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* fixed script printingGravatar corbinea2008-01-17
* Bug in sqrt321Gravatar thery2008-01-17
* Fix backtracking bugs:Gravatar lmamane2008-01-15
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Amélioration de la génération des graphes de dépendancesGravatar notin2008-01-11
* implements a better way to respect the Unix convention that processes receive...Gravatar bertot2008-01-11
* Amélioration de la génération des graphes de dépendances (utilisation de ...Gravatar notin2008-01-11
* Correction du bug #1770: il semble que la recherche insensible à la casse ne...Gravatar notin2008-01-10
* Correction of bug #1769Gravatar jforest2008-01-09
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous CoqideGravatar notin2008-01-07
* Remove spurious .d, better tactics.Gravatar msozeau2008-01-07
* Completion of 10427...Gravatar herbelin2008-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-02 02:06:29 +0000