coq - The formal proof system

Age	Commit message (Expand)	Author
2014-09-04	Make CoqIDE compile with windows (Closes: 3573)	Enrico Tassi
2014-09-04	Fix: shelve_unifiable did not work modulo evar instantiation.	Arnaud Spiwack
2014-09-04	Proofview refiner is now type-safe by default.	Pierre-Marie Pédrot
2014-09-04	Typing.sort_of does not leak evarmaps anymore.	Pierre-Marie Pédrot
2014-09-04	More explicit printing in Himsg.	Pierre-Marie Pédrot
2014-09-04	Status error for bug #3459.	Pierre-Marie Pédrot
2014-09-04	Test for bug #3459.	Pierre-Marie Pédrot
2014-09-04	Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.	Pierre-Marie Pédrot
2014-09-04	Using goal-tactics to interpret arguments to idtac.	Pierre-Marie Pédrot
2014-09-04	Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."	Pierre-Marie Pédrot
2014-09-04	Revert "Tacinterp: [interp_message] and associate now only require an environ...	Pierre-Marie Pédrot
2014-09-04	Revert "Ltac's idtac is now implemented using the new API."	Pierre-Marie Pédrot
2014-09-04	Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."	Pierre-Marie Pédrot
2014-09-04	Fix bug #3561, correct folding of env in context[] matching.	Matthieu Sozeau
2014-09-04	Fix bug #3559, ensuring a canonical order of universe level quantifications when	Matthieu Sozeau
2014-09-04	Documenting the [Variant] type definition and the [Nonrecursive Elimination S...	Arnaud Spiwack
2014-09-04	Commands like [Inductive > X := … \| … \| …] raise an error message inste...	Arnaud Spiwack
2014-09-04	Factorize the parsing rules of [Record] and the other kind of type definitions.	Arnaud Spiwack
2014-09-04	Remove [Infer] option of records.	Arnaud Spiwack
2014-09-04	Type definitions with [Variant] don't generate inductive schemes by default.	Arnaud Spiwack
2014-09-04	Type definitions [Variant] and [Record] really don't accept the wrong kind of...	Arnaud Spiwack
2014-09-04	Inductive and CoInductive records are printed correctly.	Arnaud Spiwack
2014-09-04	Types declared as Variants really do not accept recursive definitions.	Arnaud Spiwack
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-09-04	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack
2014-09-04	Add test-suite file for Case derivation on primitive records.	Matthieu Sozeau
2014-09-04	Add test suite files for closed bugs.	Matthieu Sozeau
2014-09-04	Fix bug #3563, making syntactic matching of primitive projections	Matthieu Sozeau
2014-09-03	Putting back normalized goals when entering them.	Pierre-Marie Pédrot
2014-09-03	Yes another remaining clearing bug with 'apply in'.	Hugo Herbelin
2014-09-03	Fixing printing of unreachable local tactics.	Pierre-Marie Pédrot
2014-09-03	Test-suite for bug #2818.	Pierre-Marie Pédrot
2014-09-03	Fixing bug #2818.	Pierre-Marie Pédrot
2014-09-03	Useless hooks in Tacintern.	Pierre-Marie Pédrot
2014-09-03	Code simplification in Tacenv.	Pierre-Marie Pédrot
2014-09-03	Print error messages with more hidden information based on α-equivalence .	Arnaud Spiwack
2014-09-03	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier
2014-09-03	Improve RefMan section about Coq_makefile	Pierre Boutillier
2014-09-03	Update RefMan with respect to new loadpath management	Pierre Boutillier
2014-09-03	Cbn in refman	Pierre Boutillier
2014-09-03	Additional entry tactic_arg in Print Grammar tactic.	Pierre-Marie Pédrot
2014-09-03	Code factorization in Tacintern.	Pierre-Marie Pédrot
2014-09-02	Cleaning code in Pptactic.	Pierre-Marie Pédrot
2014-09-02	Adding a test-suite for second-order matching order and indexes.	Pierre-Marie Pédrot
2014-09-02	Fixing bug #3136.	Pierre-Marie Pédrot
2014-09-02	Another fix than 19a7a5789c to avoid descend_in_conjunction to use	Hugo Herbelin
2014-09-02	An apply test.	Hugo Herbelin
2014-09-02	Fixup introduction of coqworkmgr	Pierre Boutillier
2014-09-02	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot
2014-09-02	stm: use xlabel insted of label in dot (debug) output	Enrico Tassi