aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* ZOdiv: fully use generic properties from ZDivTrunc.vGravatar letouzey2009-12-17
* Reverse order of arguments in min_case_strong for better uniformity (and comp...Gravatar letouzey2009-12-17
* Division in Numbers : more properties, new filenames based on a paper by R. B...Gravatar letouzey2009-12-17
* correction de la nouvelle option pour functional inductionGravatar jforest2009-12-16
* adding an option functional_induction_rewrite_dependent to make functional in...Gravatar jforest2009-12-16
* Division in Numbers: more properties proved (still W.I.P.)Gravatar letouzey2009-12-16
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
* file integrated into the archive by mistakeGravatar letouzey2009-12-15
* Description of the new features of the module system (part two).Gravatar soubiran2009-12-15
* Description of the new features of the module system (first part).Gravatar soubiran2009-12-15
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Completion of r12580 (better rendering of dependent rewrite and inversion).Gravatar herbelin2009-12-13
* Deactivating printing of {| |} for records when option Printing All is set.Gravatar herbelin2009-12-13
* Fixing bug in printing option as of remember and generalizeGravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Improved the rendering of "dependent rewrite" and hence of "inversion"Gravatar herbelin2009-12-12
* Deport the backtracking code out of the ideGravatar vgross2009-12-11
* NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...Gravatar letouzey2009-12-10
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...Gravatar letouzey2009-12-08
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
* integrate MSetToFiniteSet into the compilation (and fix it)Gravatar letouzey2009-12-08
* Sos.ml: no more warningsGravatar letouzey2009-12-08
* Declaremods.ml: a useless function wrongly introduced in last commitGravatar letouzey2009-12-08
* Fix bug #2197 (option show_toolbar not taken into account at startup)Gravatar vgross2009-12-07
* Remove the "detach script windows" feature.Gravatar vgross2009-12-07
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* revert on commit r12553Gravatar barras2009-12-07
* Turn evars created by a tactic application into a subgoal immediately inGravatar msozeau2009-12-06
* Forgot a file in last commit.Gravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)Gravatar herbelin2009-12-03
* Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameGravatar herbelin2009-12-03
* Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
* declaremods.ml <--- code factoringGravatar soubiran2009-12-03
* Rename proper to proper_prf to avoid clash with CoRN, Gravatar msozeau2009-12-03
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Remove interface pluginGravatar glondu2009-12-02
* Update .gitignoreGravatar glondu2009-12-02
* two improvements of the guard condition:Gravatar barras2009-12-01
* fix coqchk options documentationGravatar barras2009-12-01
* install manpage of coqchkGravatar barras2009-12-01
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Fix bug in typeclass resolution. Better handling of universes inGravatar msozeau2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 05:12:41 +0000