aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix typos in commentsGravatar glondu2009-09-17
* Clarify documentation of ltac repeatGravatar glondu2009-09-17
* - Tentatively made order-dependency wrt .vo files a full dependencyGravatar herbelin2009-09-15
* Fix compilation errors due to last commit.Gravatar msozeau2009-09-15
* Dont't forget to update the state or an obligation tactic assignment mayGravatar msozeau2009-09-15
* Fixed compilation error message which was no longer emacs-compliant sinceGravatar herbelin2009-09-15
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* removed the double-click / proof hiding association.Gravatar vgross2009-09-14
* tags refactoringGravatar vgross2009-09-14
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Addendum to revision 12323; update Makefile.common after removal ofGravatar herbelin2009-09-11
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Add doc of [Context] vernacular.Gravatar msozeau2009-09-11
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* Removed Gappa from the external provers supported by the dp plugin. Tactic ga...Gravatar gmelquio2009-09-11
* - Resolve type class constraints before trying to find unresolvedGravatar msozeau2009-09-11
* Fixes for toc depth handling and handling of substitles from Chris Casinghino.Gravatar msozeau2009-09-10
* Misc fixes:Gravatar msozeau2009-09-10
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Allow setoid rewrite to rewrite in pattern-matching scrutinees orGravatar msozeau2009-09-09
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* Stop trying to search if the relation is declared as a [RewriteRelation]Gravatar msozeau2009-09-09
* Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchGravatar msozeau2009-09-08
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* ajout CVC3; ajout traduction des reelsGravatar marche2009-09-07
* Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,Gravatar msozeau2009-09-04
* Add --plain-comments patch by F. Garillot, which also addsGravatar msozeau2009-09-03
* Support globality flag properly for "Add Morphism foo : foo_mor" syntax.Gravatar msozeau2009-09-03
* Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], asGravatar msozeau2009-09-03
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
* Hack to correctly get ill-formed rec body exceptions even Gravatar msozeau2009-09-02
* Fix notation for ~x in theories/Unicode/Utf8.vGravatar glondu2009-08-31
* Fix minor spelling errorGravatar glondu2009-08-29
* update for why 2.19Gravatar marche2009-08-28
* Correction bug 2140.Gravatar soubiran2009-08-27
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...Gravatar fbesson2009-08-25
* Delegate _all_ doc targets to stage2Gravatar lmamane2009-08-25
* install-doc* are PHONYGravatar lmamane2009-08-25
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
* Fix a small oversight in checker commit 12288.Gravatar herbelin2009-08-23
* Transfers to checker ("let"s in inductive arities + Coq root read-only).Gravatar herbelin2009-08-22
* new csdp cache + improved error messageGravatar fbesson2009-08-20
* new csdp cache + improved error messageGravatar fbesson2009-08-20
* adds a property on mapGravatar bertot2009-08-19
* adds lemmas on interactions between existsb, forallb, and appGravatar bertot2009-08-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:33:20 +0000