aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Only using filtered hyps in Goal.enter.Gravatar Pierre-Marie Pédrot2014-09-04
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Reimplementing the clearbody tactic.Gravatar Pierre-Marie Pédrot2014-09-04
* Make CoqIDE compile with windows (Closes: 3573)Gravatar Enrico Tassi2014-09-04
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-09-04
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tacinterp: [interp_message] and associate now only require an environ...Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's idtac is now implemented using the new API."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Gravatar Arnaud Spiwack2014-09-04
* Commands like [Inductive > X := … | … | …] raise an error message inste...Gravatar Arnaud Spiwack2014-09-04
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Type definitions with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
* Type definitions [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Inductive and CoInductive records are printed correctly.Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* Add test-suite file for Case derivation on primitive records.Gravatar Matthieu Sozeau2014-09-04
* Add test suite files for closed bugs.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3563, making syntactic matching of primitive projectionsGravatar Matthieu Sozeau2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Fixing printing of unreachable local tactics.Gravatar Pierre-Marie Pédrot2014-09-03
* Test-suite for bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Fixing bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Code simplification in Tacenv.Gravatar Pierre-Marie Pédrot2014-09-03
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
* Improve RefMan section about Coq_makefileGravatar Pierre Boutillier2014-09-03
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
* Cbn in refmanGravatar Pierre Boutillier2014-09-03
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
* Code factorization in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
* Adding a test-suite for second-order matching order and indexes.Gravatar Pierre-Marie Pédrot2014-09-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-15 18:56:17 +0000