coq - The formal proof system

Age	Commit message (Expand)	Author
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
2011-04-06	Fix dev/base_include after change of constant_body	letouzey
2011-04-06	Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.	aspiwack
2011-04-06	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey
2011-04-03	Update documentation concerning proofs loading (cf last commit)	letouzey
2011-04-03	Fix last commit about coqdep: not everyone has a user-contrib dir	letouzey
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-04-03	Quickly avoid global axioms in Loic new files about ring	letouzey
2011-04-01	Adjust coqdep so that it behaves like coqtop with respect to the user-contrib...	gmelquio
2011-04-01	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey
2011-04-01	Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)	letouzey
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2011-03-31	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin
2011-03-31	Extraction: customized inductives are always standard	glondu
2011-03-30	Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)	letouzey
2011-03-30	Coqide: avoid confusion of process when restarting coqtop + cosmetic	letouzey
2011-03-30	Ide_intf: documentation of calls + debug printing of calls/answers	letouzey