aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Various subtac fixes.Gravatar msozeau2007-01-15
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
* un saut de ligne ...Gravatar letouzey2007-01-12
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
* suite de la reparation du bug 1239: apres les inds, les records et vars de typesGravatar letouzey2007-01-05
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
* Default tactic for solving goals.Gravatar msozeau2006-12-22
* typo malencontreuseGravatar filliatr2006-12-21
* reparation bug 1239Gravatar letouzey2006-12-17
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* contrib/dp: tactique ergo (voir ergo.lri.fr)Gravatar filliatr2006-12-15
* Reimplemented equality generation for pattern matching at typing time. First ...Gravatar msozeau2006-12-14
* Subtac: work on cases.Gravatar msozeau2006-12-12
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* contrib/dpGravatar filliatr2006-12-08
* Subtac bug fix, add list take example.Gravatar msozeau2006-12-08
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* Functional graph merging deals with letins.Gravatar courtieu2006-11-24
* Fixed the graph merging parameter order.Gravatar courtieu2006-11-24
* Fixing syntax and parameter order in functional graph merging.Gravatar courtieu2006-11-23
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* Changing merging functional scheme syntax.Gravatar courtieu2006-11-20
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* mult_sym, plus_sym -> mult_comm, plus_commGravatar herbelin2006-11-19
* Small fix in functional graph merging.Gravatar courtieu2006-11-16
* suppression de code mort (avec bug de nom)Gravatar letouzey2006-11-16
* pb avec r9379 + modifs dans ringGravatar barras2006-11-16
* Work on dep types pattern matchingGravatar msozeau2006-11-16
* suite de r9362: reconnaissance de qqs injections entre nat, N et ZGravatar barras2006-11-16
* Some usability enhancements.Gravatar msozeau2006-11-15
* Better solve using tactics impl.Gravatar msozeau2006-11-13
* Correction de la seconde partie du bug #1278Gravatar jforest2006-11-13
* Correction de la premiere partie du #1278 (but non referme en cas d'echec)Gravatar jforest2006-11-13
* Encore des _sym au lieu de _commGravatar herbelin2006-11-13
* generalisation de ring pour faire Ring_nfGravatar barras2006-11-10
* Work on mutual defs, various bug fixes.Gravatar msozeau2006-11-10
* Work on pattern inequalities for pattern matching branches.Gravatar msozeau2006-11-10
* Support for mutual defs in obligation handling.Gravatar msozeau2006-11-09
* Debug obligation handling codeGravatar msozeau2006-10-31
* Fix compile errorGravatar msozeau2006-10-31
* Work on obligation separation.Gravatar msozeau2006-10-31
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* Suite commit polymorphismeGravatar herbelin2006-10-29
* Exports manquants dans ringGravatar barras2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Fixes in experimental merging of functional graphs.Gravatar courtieu2006-10-28
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:29:22 +0000