aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.Gravatar gmelquio2009-09-28
* Apply "Declare Implicit Tactic" also to terms interpreted as "openGravatar herbelin2009-09-27
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.Gravatar herbelin2009-09-27
* Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.Gravatar herbelin2009-09-27
* Fixed error message "cannot infer the type of id" in presence ofGravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Complement to 12347 and 12348 on the extended syntax of case/elim.Gravatar herbelin2009-09-27
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Micromega doc : psatz Z -> psatz Z 2Gravatar fbesson2009-09-24
* Ltac doc: only variables are accepted as message_tokenGravatar glondu2009-09-23
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
* Better use of transparency information for local hypotheses: Gravatar msozeau2009-09-22
* Update link to "Recursive Make Considered Harmful"Gravatar glondu2009-09-21
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
* micromega: better handling of exponentiation + correction of test-suite termi...Gravatar fbesson2009-09-18
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Replace call to where_in_path by find_file_in_path in "Locate File"Gravatar glondu2009-09-17
* Replace unprotected call to where_in_path by find_file_in_pathGravatar glondu2009-09-17
* Remove useless MonoList.vGravatar glondu2009-09-17
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 05:33:22 +0000