aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-02-05Ajout d'un test pour le bug #1787notin
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
2008-02-04Instantiation of evars after instantiate (closes #1672).glondu
2008-02-04declaremods.mlsoubiran
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
2008-02-02fix the syntax "Include Type Foo"letouzey
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...letouzey
2008-02-01Ajout de 2 testsnotin
2008-02-01Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak...letouzey
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-02-01Suite révision 10495herbelin
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-31Fix obvious syntax error. Forgot to recompile before commiting...msozeau
2008-01-31Remove unneeded .d mask, can be set localy by each dev inmsozeau
2008-01-31Ignore generated dependency files.msozeau
2008-01-31Debug implementation of dependent induction/dependent destruction and documen...msozeau
2008-01-31Finish let| implementation and document itmsozeau
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding tactic...msozeau
2008-01-30Use new redefinition support for the default obligations tacticmsozeau
2008-01-30Support for substructures in classes using :> notationmsozeau
2008-01-30Add occurence extra argmsozeau
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
2008-01-30Add list_iter3 msozeau
2008-01-30Add some keywordmsozeau
2008-01-29Added full documentation for mathematical mode (draft version)corbinea
2008-01-29Correction du bug #1785notin
2008-01-24Nicer proofs.roconnor
2008-01-24remove Fourier Failure warnings.roconnor
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
2008-01-24Fermeture du bug #1754notin
2008-01-24Keep the Z_scope local to this file.roconnor
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
2008-01-23Ajout d'un test pour le bug #1779notin
2008-01-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
2008-01-23Typonotin
2008-01-22Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)notin
2008-01-22Adding Zdiv_le_compat_lthery
2008-01-22Récupération d'une exception Not_foundnotin
2008-01-21Correction du bug #1754notin
2008-01-20cosmetics: after an extract inductive to bool, let's use if then elseletouzey
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-18bug in accessing n-th abstractionbarras
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-17Fix Makefile bug, using .v instead of .vo and document SetoidDec.vmsozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-17fixed script printingcorbinea
2008-01-17Bug in sqrt321thery
2008-01-15Fix backtracking bugs:lmamane
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau