aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* use only why-dp, support for z3Gravatar marche2009-11-10
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Make usage of Dyn explicitGravatar glondu2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix for missing hypotesae in XML proof tree export.Gravatar cek2009-10-07
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Fixed small name freshness bug in Functional Scheme ("Heq" name wasGravatar herbelin2009-10-03
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* micromega: better handling of exponentiation + correction of test-suite termi...Gravatar fbesson2009-09-18
* 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