coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-30	Fixed small bugs introduced in commit 12890 (bug #2286, that comes	herbelin
2010-03-30	Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i...	letouzey
2010-03-30	Improving error messages in the presence of utf-8 characters	herbelin
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2010-03-28	Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic	herbelin
2010-03-28	Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)	herbelin
2010-03-27	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin
2010-03-27	Applied greenrd's patch to fix bug 2255 (injection failed to	herbelin
2010-03-24	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin
2010-03-23	Updated CHANGES wrt 8.3	herbelin
2010-03-23	Added automatic expansion on the left of recursive notations	herbelin
2010-03-23	Changing types to reflect futur separation between toplevel and ide.	vgross
2010-03-23	infrastructure for safe marshal-based IPC	vgross
2010-03-23	Goal generation deported into ide/coq.ml, single function to obtain	vgross
2010-03-23	New functions for goals fetching.	vgross
2010-03-23	Fix bug in backtracking.	vgross
2010-03-23	debugging	vgross
2010-03-19	Removing unexpected printing of debug output (see bug report #2271).	herbelin
2010-03-19	Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu...	notin
2010-03-18	kills a warning about vo in checker/safe_typing	letouzey
2010-03-18	Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/...	letouzey
2010-03-18	Myocamlbuild: slight simplification of code for .ml4	letouzey
2010-03-15	Oops, don't use zeta by default.	msozeau
2010-03-15	Stop dropping evar constraints when building a new goal evar defs.	msozeau
2010-03-15	Fix splitting evars tactics and stop dropping evar constraints when	msozeau
2010-03-12	fixed minor pbs with test cases	barras
2010-03-12	fixed confusion between number of cstr arguments and number of pattern variab...	barras
2010-03-11	introduced lazy computation of size info in the guard condition	barras
2010-03-11	Update manual on search commands	puech
2010-03-11	Minimal test suite for search commands	puech
2010-03-11	fix [Search] when the result has no hypothesis & constant comparison	puech
2010-03-11	No delta-reduction in libtypes anymore	puech
2010-03-11	Filter out "_subproof" objects from search results	puech
2010-03-10	NMake: remove useless tactics abstract_pair, nicer comments	letouzey
2010-03-10	NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...	letouzey
2010-03-10	NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftl	letouzey
2010-03-08	Consider OccurCheck a catchable exception.	msozeau
2010-03-08	Application des patches envoyés par F. Besson pour micromega	notin
2010-03-07	Reorder resolution of type class and unification constraints.	msozeau
2010-03-07	Fix lifting of constraints in generalized rewriting tactic.	msozeau
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-03-06	Adding Function as keyword for coqdoc	thery
2010-03-05	Makefile: some more cleanup	letouzey
2010-03-05	Minor fixes.	msozeau
2010-03-05	Improvements in generalized rewriting:	msozeau
2010-03-05	Fix [autounfold] to accept general [in] clauses.	msozeau
2010-03-05	Add a generic tactic option builder. Use it in firstorder to set the	msozeau
2010-03-04	Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi (t...	letouzey
2010-03-04	Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...	letouzey