aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Dont't forget to update the state or an obligation tactic assignment mayGravatar msozeau2009-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
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-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
* Misc fixes:Gravatar msozeau2009-09-10
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* ajout CVC3; ajout traduction des reelsGravatar marche2009-09-07
* 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
* update for why 2.19Gravatar marche2009-08-28
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...Gravatar fbesson2009-08-25
* new csdp cache + improved error messageGravatar fbesson2009-08-20
* new csdp cache + improved error messageGravatar fbesson2009-08-20
* +Fix interface.Gravatar aspiwack2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Infix (r12268 continued)Gravatar herbelin2009-08-11
* 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
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* addition of lia.cache - csdp.cache is now handled by micromega not csdpcertGravatar fbesson2009-07-31
* micromega : Better parsing of formulae - smaller proof terms for Z - redesign...Gravatar fbesson2009-07-30
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Use camlp4 to accept some specific non-exhaustive patterns in groebnerGravatar letouzey2009-07-20
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* repport of commit r12221Gravatar jforest2009-07-04
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
* Fix bug introduced by last revision, subtac_cases was returning theGravatar msozeau2009-06-29
* Abstract the tycon by the matched terms when turning them into variablesGravatar msozeau2009-06-28
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Fallback on not using [fix_proto] if the right imports aren't there, the Gravatar msozeau2009-06-17
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Fix de Bruijn lifting bug appearing when we match on multiple terms withGravatar msozeau2009-05-26
* Support for definition hooks in subtac.Gravatar msozeau2009-05-16
* micromega: proof compression bugfixGravatar fbesson2009-05-11
* More efficient handling of evars in Program Fixpoint commands.Gravatar msozeau2009-04-28
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* - New cleaning phase for the entry points of pretyping.mlGravatar herbelin2009-04-24