aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Move definition of VO_TOOLS_DEP before first use of it.Gravatar lmamane2007-01-17
* Reintroduce compatibility with old versions of GNU makeGravatar lmamane2007-01-17
* Correction bug #1282Gravatar herbelin2007-01-17
* Correction bug #1302Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
* README update:Gravatar lmamane2007-01-17
* 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
* addition du neq unicodeGravatar letouzey2007-01-12
* Petit oubli dans commit 9474Gravatar herbelin2007-01-11
* Ajout d'une option de débogage pour expliciter l'instance des evarsGravatar herbelin2007-01-11
* - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)Gravatar lmamane2007-01-10
* Merge with Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-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
* Add f_equal case for 6 arguments.Gravatar msozeau2007-01-02
* Protection contre une source possible de liaison de lambda anonymeGravatar herbelin2006-12-29
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
* Correction petits bugs du check de la test-suiteGravatar herbelin2006-12-28
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
* Report correction bug #1289 dans trunk (r9435 pour branche v8.1)Gravatar herbelin2006-12-26
* Doc for Combined Scheme.Gravatar msozeau2006-12-23
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* Default tactic for solving goals.Gravatar msozeau2006-12-22
* remplacement d'un test d'egalite par un test de convertibilite dans injection...Gravatar jforest2006-12-22
* typo malencontreuseGravatar filliatr2006-12-21
* Adaptation à Subversion 1.4Gravatar notin2006-12-19
* 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
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
* Reimplemented equality generation for pattern matching at typing time. First ...Gravatar msozeau2006-12-14
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* test condition de gardeGravatar barras2006-12-13
* svn:ignoreGravatar herbelin2006-12-13
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
* Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...Gravatar notin2006-12-12
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* Subtac: work on cases.Gravatar msozeau2006-12-12
* nouvelle indentation des scriptsGravatar barras2006-12-12
* cosmetiqueGravatar barras2006-12-12
* Variable print_instances pour déboguer les instances d'evarGravatar herbelin2006-12-12
* Dépendence inutileGravatar herbelin2006-12-12