aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* Makefile: ml dependencies of contribs are moved to .mllib filesGravatar letouzey2009-03-14
* Cleanup: remove old correctness files, unused for a long timeGravatar letouzey2009-03-11
* fixed groebner as a plugin + pattern matching TimeoutGravatar barras2009-03-06
* missing RequireGravatar barras2009-03-06
* oups (module Entiers remplace par Big_int)Gravatar barras2009-03-06
* ajout de la tactique groebner de Loic PottierGravatar barras2009-03-05
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* extraction: update of README+CHANGES, rm of BUGS+TODOGravatar letouzey2009-02-27
* coq-interface and coq-parser can be calls to coqtop with adequate code dynlinkGravatar letouzey2009-02-20
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Allow to turn contrib/subtac into a (nat)dynlink'able pluginGravatar letouzey2009-02-03
* Forgot a file in r11859. Sorry...Gravatar puech2009-01-27
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
* Fix #2011 : an incorrect environment when extracting Module ... with ...Gravatar letouzey2009-01-22
* Extraction Library works now when some files share the same short name (fix #...Gravatar letouzey2009-01-22
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Fixing #1960 (xml bug with external on goal variable) and #1961Gravatar herbelin2009-01-14
* Moved JProver to a user contribution (as was decided a long time ago)Gravatar herbelin2009-01-04
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* 11715 continuedGravatar herbelin2008-12-26
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Désactivation de dumpglob lors des appels a functional induction (erreurs pa...Gravatar notin2008-12-18
* Avoid printing that extraction has created file Foo when it's not the caseGravatar letouzey2008-12-17
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
* Extraction: also comply to Set Printing Width when producing external filesGravatar letouzey2008-12-16
* Take advantage of natdynlink when available: almost all contribs become loada...Gravatar letouzey2008-12-16
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of Gravatar herbelin2008-12-10
* About "apply in":Gravatar herbelin2008-12-09
* Correct handling of defined methods (let-ins) in instance declarations.Gravatar msozeau2008-12-04
* fixed non-exhaustive pattern matchingGravatar barras2008-11-27
* amelioration mineur du comportement de FunctionGravatar jforest2008-11-24
* first attempt to allow Function to deal with dependent pattern matching. This...Gravatar jforest2008-11-23
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 05:52:38 +0000