aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fixing bug #3136.Gravatar Pierre-Marie Pédrot2014-09-02
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* An apply test.Gravatar Hugo Herbelin2014-09-02
* Fixup introduction of coqworkmgrGravatar Pierre Boutillier2014-09-02
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* stm: use xlabel insted of label in dot (debug) outputGravatar Enrico Tassi2014-09-02
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
* Removing the 'inductive' parameter from tacexpr AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* In evarconv, do first-order unification of LetIn's properly, ensuring we comp...Gravatar Matthieu Sozeau2014-09-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-20 22:03:23 +0000