coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-08	Consider OccurCheck a catchable exception.	msozeau
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-04	Errors issued by reduction tactics (e.g. pattern) were not caught by "try".	herbelin
2009-12-30	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-22	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-21	In "progress", extending the set of evars w/o solving an existing one is	herbelin
2009-12-19	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-30	Take constraints into account in the "instantiate" tactic	herbelin
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-10-27	fixed czar bug with parametric inductives	corbinea
2009-10-25	Add support for remaining side-conditions in "apply in as".	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	herbelin
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-06	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin
2009-06-02	Backtrack on experimental unification with sort variables: it requires	msozeau
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-18	Minor unification changes:	msozeau
2009-04-24	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2009-01-23	Really compare evar maps in progress, due to merging in apply and other	msozeau
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau