coq - The formal proof system

Age	Commit message (Expand)	Author
2011-04-20	Don't force progress on instance applications, there is always progress when ...	msozeau
2011-04-20	This is used in the rippling plugin. This also allows fixing bug #2188.	msozeau
2011-04-19	Declarative mode: fix escape and return.	aspiwack
2011-04-19	Fix thumb2-related build error	glondu
2011-04-18	Fix generated script for NMake, a rewrite necessitates full conversion for	msozeau
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-16	Fix unification of types of metavariables and error message for sort unificat...	msozeau
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-04-15	Coqc: fix the exit code	letouzey
2011-04-15	Extraction: nicer error when a toplevel module has no body (#2525)	letouzey
2011-04-15	Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)	letouzey
2011-04-15	Documentation typo.	gmelquio
2011-04-14	More informative anomaly.	herbelin
2011-04-14	Add directories in COQPATH to search path.	herbelin
2011-04-14	Reorder search path order, so the standard library is search last.	herbelin
2011-04-13	Extraction: opaque terms are not traversed anymore by default	letouzey
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Put dependent subgoals first so as to allow backtracking on them, might chang...	msozeau
2011-04-13	- Make typeclass transparency information directly available	msozeau
2011-04-13	- Remove create_evar_defs	msozeau
2011-04-13	Fix merge.	msozeau
2011-04-13	- Improve unification (beta-reduction, and same heuristic as evarconv for red...	msozeau
2011-04-13	Fix scripts relying on unification not doing any beta reduction.	msozeau
2011-04-13	Unify meta types with the right flags, add betaiotazeta reduction to unificat...	msozeau
2011-04-13	Proper typing of metavariables, type errors were completely ignored before......	msozeau
2011-04-13	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-12	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey
2011-04-12	remove old traces of SearchIsos (never ported to 7.x nor 8.x)	letouzey
2011-04-11	Catch NotArity exception and transform it into an anomaly in retyping.	msozeau
2011-04-08	ocamlbuild: support again camlp5 in addition to camlp4	letouzey
2011-04-08	Applying Tom Prince's patch to coqdep not correctly applying the -R visibility	herbelin
2011-04-08	A kind of reply to bug 2444	pboutill
2011-04-08	weak dependency of coqtop for coqide and coqc (bug 2390)	pboutill
2011-04-08	A module out of Program to have list notations (bug 2463)	pboutill
2011-04-08	@ in index of refman (last request of bug 2494)	pboutill
2011-04-08	Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395	pboutill
2011-04-08	More up to date About in coqide	pboutill
2011-04-08	Macos integration step2 : shutdown	pboutill
2011-04-08	coqide shutdown process change (and out the main function)	pboutill
2011-04-08	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin
2011-04-08	Made warning about ending comments in string less intrusive so as to support	herbelin
2011-04-08	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin
2011-04-08	Replaced printing number of ill-typed branch by printing name of constructor	herbelin
2011-04-08	Fixed "Eval ... in t" when t has still metavariables.	herbelin
2011-04-08	Fixing multiple printing bugs with "Notation f x := ..."	herbelin
2011-04-07	Extraction: unfolds the let-in created by Program when handling "match"	letouzey
2011-04-07	Extraction: avoid some useless Obj.magic by fixing my ML type unifier	letouzey
2011-04-06	Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)	herbelin
2011-04-06	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin