aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-03Update RefMan with respect to new loadpath managementPierre Boutillier
2014-09-03Cbn in refmanPierre Boutillier
2014-09-03Additional entry tactic_arg in Print Grammar tactic.Pierre-Marie Pédrot
2014-09-03Code factorization in Tacintern.Pierre-Marie Pédrot
2014-09-02Cleaning code in Pptactic.Pierre-Marie Pédrot
2014-09-02Adding a test-suite for second-order matching order and indexes.Pierre-Marie Pédrot
2014-09-02Fixing bug #3136.Pierre-Marie Pédrot
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
2014-09-02An apply test.Hugo Herbelin
2014-09-02Fixup introduction of coqworkmgrPierre Boutillier
2014-09-02Removing [revert] tactic from the AST.Pierre-Marie Pédrot
2014-09-02stm: use xlabel insted of label in dot (debug) outputEnrico Tassi
2014-09-02coqworkmgrEnrico Tassi
2014-09-02Fix Declaremods.end_library (Closes: #3536)Enrico Tassi
2014-09-01Removing the 'inductive' parameter from tacexpr AST.Pierre-Marie Pédrot
2014-09-01Moving the decompose tactic out of the AST.Pierre-Marie Pédrot
2014-09-01In evarconv, do first-order unification of LetIn's properly, ensuring we comp...Matthieu Sozeau
2014-09-01Coqide prints succesive hyps of the same type on 1 linePierre Boutillier
2014-09-01Code cleaning in Tacintern.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-29Simplification of Genarg unpackers.Pierre-Marie Pédrot
2014-08-29Not using a "cut" in descend_in_conjunctions induced more success. WeHugo Herbelin
2014-08-29Fixing commit 50237af2.Pierre-Marie Pédrot
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
2014-08-29Fix bug when defining primitive projections mixing defined and abstracts fields.Matthieu Sozeau
2014-08-28Fixing bug #3528.Pierre-Marie Pédrot
2014-08-28Simplification of the tclCHECKINTERRUPT tactic.Pierre-Marie Pédrot
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
2014-08-28There are some occurs-check cases that can be handled by imitation (using pru...Matthieu Sozeau
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
2014-08-28Cleaning and documenting a bit the Proofview.Refine module.Pierre-Marie Pédrot
2014-08-28Adding test-suite for bug #3212.Pierre-Marie Pédrot
2014-08-28Fixing bug #3541.Pierre-Marie Pédrot
2014-08-27Protect against "it's unifiable, if you solve some unsolvable constraints" be...Matthieu Sozeau
2014-08-27Removing spurious tclWITHHOLES.Pierre-Marie Pédrot
2014-08-27Fixing bug #3493.Pierre-Marie Pédrot
2014-08-26Add a regression test for 3427Jason Gross
2014-08-26Prove forall extensionalityJason Gross
2014-08-26Add t-jagro to .mailmapJason Gross
2014-08-26Distributed binaries under MacOS are signed.Pierre Boutillier
2014-08-26Configure.ml creates metadata to annotate MacOS binariesPierre Boutillier
2014-08-26Debug RAKAMPierre Boutillier
2014-08-26sed s'/_one_var/_on/g'Jason Gross
2014-08-26Generalize EqdepFactsJason Gross
2014-08-26Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inMatthieu Sozeau
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:43:16 +0000