aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* + csdp.cacheGravatar fbesson2009-08-15
* Mise à jour du document de révision de la stdlib et déplacement de laGravatar herbelin2009-08-14
* +Fix interface.Gravatar aspiwack2009-08-14
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
* Tried to make F1 documentation tool working in CoqIDE.Gravatar herbelin2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Made unification patch 12268 even more ad hoc (if evars remain in aGravatar herbelin2009-08-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Ajout des .annot dans le .gitignore.Gravatar aspiwack2009-08-11
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
* Infix (r12268 continued)Gravatar herbelin2009-08-11
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* changed deprecated setoid into relationGravatar amahboub2009-08-05
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Fixed subst failing when a truly heterogeneous JMeq hyp is in theGravatar herbelin2009-08-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 18:39:21 +0000