aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2007-01-22Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentherbelin
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
2007-01-15Various subtac fixes.msozeau
2007-01-12Suite au mail de Lionel a propos du Makefile: letouzey
2007-01-12un saut de ligne ...letouzey
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
2007-01-05suite de la reparation du bug 1239: apres les inds, les records et vars de typesletouzey
2007-01-02Rework subtac pattern matching equalities generation.msozeau
2006-12-28Remplacement de la définition de Pind et Prec par une définitionherbelin
2006-12-22Default tactic for solving goals.msozeau
2006-12-21typo malencontreusefilliatr
2006-12-17reparation bug 1239letouzey
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ...msozeau
2006-12-12Subtac: work on cases.msozeau
2006-12-11Changement dans le kernel : bgregoir
2006-12-08contrib/dpfilliatr
2006-12-08Subtac bug fix, add list take example.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-11-24Functional graph merging deals with letins.courtieu
2006-11-24Fixed the graph merging parameter order.courtieu
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
2006-11-20Changing merging functional scheme syntax.courtieu
2006-11-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
2006-11-19mult_sym, plus_sym -> mult_comm, plus_commherbelin
2006-11-16Small fix in functional graph merging.courtieu
2006-11-16suppression de code mort (avec bug de nom)letouzey
2006-11-16pb avec r9379 + modifs dans ringbarras
2006-11-16Work on dep types pattern matchingmsozeau
2006-11-16suite de r9362: reconnaissance de qqs injections entre nat, N et Zbarras
2006-11-15Some usability enhancements.msozeau
2006-11-13Better solve using tactics impl.msozeau
2006-11-13Correction de la seconde partie du bug #1278jforest
2006-11-13Correction de la premiere partie du #1278 (but non referme en cas d'echec)jforest
2006-11-13Encore des _sym au lieu de _commherbelin
2006-11-10generalisation de ring pour faire Ring_nfbarras
2006-11-10Work on mutual defs, various bug fixes.msozeau
2006-11-10Work on pattern inequalities for pattern matching branches.msozeau
2006-11-09Support for mutual defs in obligation handling.msozeau
2006-10-31Debug obligation handling codemsozeau
2006-10-31Fix compile errormsozeau
2006-10-31Work on obligation separation.msozeau
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
2006-10-29Suite commit polymorphismeherbelin
2006-10-29Exports manquants dans ringbarras
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin