aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* - 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
* correction of bug #2002Gravatar jforest2008-11-20
* f_equal : solve an inefficiency issue (apply vs. simple apply)Gravatar letouzey2008-11-09
* better fix for #1931 by using sort_ofGravatar letouzey2008-11-09
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Add the ability to give a specific tactic to solve each obligation inGravatar msozeau2008-11-07
* Cosmetic: no more whitespace at end of lines in extraction filesGravatar letouzey2008-11-06
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Suite commit 11539 sur notation Record dans (Co)Inductive (MAJGravatar herbelin2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Better extraction renaming phase (fix #1914 plus other non-reported bugs)Gravatar letouzey2008-11-05
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* adding an option Function_raw_tcc to FunctionGravatar jforest2008-10-26
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* warning message when a qualid to extract can be both a module or a cstGravatar letouzey2008-10-21
* Suite 11472Gravatar herbelin2008-10-19
* Extraction of Module with eq = ... : fix for bug #1853Gravatar letouzey2008-10-16
* Extraction of mutual types with alias: fix for bug #1965Gravatar letouzey2008-10-16
* Attempt to clarify Extract_env.extract_seb_specGravatar letouzey2008-10-16
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Partial fix for bug #1948: recompute order of dependencies betweenGravatar msozeau2008-09-25
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* Fix bug #1931 by searching for a sort after doing beta,iota,delta-Gravatar msozeau2008-09-14
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Some more debugging of [Equations], unification still not perfect.Gravatar msozeau2008-09-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 07:49:04 +0000