aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac
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
* 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
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Make usage of Dyn explicitGravatar glondu2009-10-28
* 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
* 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
* - Resolve type class constraints before trying to find unresolvedGravatar msozeau2009-09-11
* Misc fixes:Gravatar msozeau2009-09-10
* Hack to correctly get ill-formed rec body exceptions even Gravatar msozeau2009-09-02
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* 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
* 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
* More efficient handling of evars in Program Fixpoint commands.Gravatar msozeau2009-04-28
* 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
* Better Requires in Classes. Fix bug #2093: the code does not requireGravatar msozeau2009-04-16
* Experimental support for automatic destruction of recursive calls andGravatar msozeau2009-04-08
* Fix bug #2083 for good: verify that the measure and relation areGravatar msozeau2009-04-08
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Fixes in Program: Gravatar msozeau2009-04-07
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Fixes in Program well-founded definitions:Gravatar msozeau2009-03-26
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20