aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
* svn:ignore propertyGravatar herbelin2009-11-26
* Fixing xml theory file export (was not consistent with coqdoc fileGravatar herbelin2009-11-26
* Fix for notation scope & inductive typesGravatar vsiles2009-11-25
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Small extra result on JMeq vs eq_dep.Gravatar herbelin2009-11-24
* Ergonomy and robustness fixGravatar vgross2009-11-23
* Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...Gravatar puech2009-11-21
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
* Correction du bug #2118 (Coqdep does not escape #)Gravatar notin2009-11-19
* Now "Include Self <expr>" handles partially applied functors, cf for example ...Gravatar soubiran2009-11-18
* Diamond-shape instead of linear hiearchy in Numbers/NatIntGravatar letouzey2009-11-18
* Allow interactive proofs in module typesGravatar letouzey2009-11-18
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
* Fix type class discharge again.Gravatar msozeau2009-11-15
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Fix [Instance: forall ..., C args := t] declarations to behave asGravatar msozeau2009-11-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:44:56 +0000