aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
2010-03-01amelioration mineure dans Functionjforest
2010-02-24correction of bug #2088jforest
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-16correction de la nouvelle option pour functional inductionjforest
2009-12-16adding an option functional_induction_rewrite_dependent to make functional in...jforest
2009-12-12Fixed incorrect computation of possible guard in presence of `{ ... } contexts.herbelin
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-21This big commit addresses two problems:soubiran
2009-10-03Fixed small name freshness bug in Functional Scheme ("Heq" name washerbelin
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-04repport of commit r12221jforest
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey