aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-07Merge pull request #15 from ejgallego/add_travisYves Bertot
2018-11-06Merge pull request #14 from ppedrot/coqpp-portEmilio Jesús Gallego Arias
2018-11-06[travis] Add Travis File.Emilio Jesus Gallego Arias
2018-11-05Port to coqpp.Pierre-Marie Pédrot
2018-11-05Merge pull request #12 from SkySkimmer/command-attsYves Bertot
2018-11-02Fix for coq/coq#8515 (command driven attributes)Gaëtan Gilbert
2018-10-31Revert "Merge pull request #13 from herbelin/master+adapt-coq8718-declaration...Yves Bertot
2018-10-30Merge pull request #13 from herbelin/master+adapt-coq8718-declaration-hooksYves Bertot
2018-10-30Adapting to Coq PR #8718: declare_definition now takes a UState.t.Hugo Herbelin
2018-10-29Merge pull request #10 from mattam82/pr8671-fixYves Bertot
2018-10-26PR 8671: Remove store / goal extra argumentMatthieu Sozeau
2018-10-22Merge pull request #11 from ejgallego/vernac+monify_hookYves Bertot
2018-10-11[coq] Adapt for PR #8704.Emilio Jesus Gallego Arias
2018-10-01fix deprecation warningsYves Bertot
2018-10-01adapts to master on Oct. 1st 2018, but warnings remainYves Bertot
2018-07-18the same license as for the coq developmentYves Bertot
2018-05-30Merge branch 'remove_constr_of_global'Yves Bertot
2018-05-30remove warnings and merge printing function for econstr termsYves Bertot
2018-05-30remove uses of Universes.constr_of_globalYves Bertot
2018-05-30this version has no warnings when compilingYves Bertot
2018-05-30Merge pull request #6 from maximedenes/fix-printerYves Bertot
2018-05-28Use user printer for terms instead of debug printerMaxime Dénès
2018-05-17Merge pull request #5 from gares/fix/tuto2Yves Bertot
2018-05-17Merge pull request #4 from gares/fix/tuto0Yves Bertot
2018-05-17Merge pull request #3 from gares/patch-1Yves Bertot
2018-05-17[tuto2] Clarify where the name of the ML plugin is usedEnrico Tassi
2018-05-17add little testEnrico Tassi
2018-05-17DECLARE PLUGIN "$name" === Declare ML Module "$name"Enrico Tassi
2018-05-17Add some setup instructionsEnrico
2018-05-17Merge pull request #2 from gares/gares-patch-1Yves Bertot
2018-05-17[tuto1] Minor fixes to commentsEnrico
2018-05-12adds a hello world tactic in tuto0Yves Bertot
2018-05-11Updates the contents of the third tutorialYves Bertot
2018-05-11This version contains documentation for the code of the packing tacticYves Bertot
2018-05-11Adds a tactic that hides the contents of an hypothesis from viewYves Bertot
2018-05-11Use the more colloquial EConstr.t type instead of EConstr.constrYves Bertot
2018-05-10This version has type inference performing proofs, using both type classesYves Bertot
2018-05-10finished the example where type class resolution is forcedYves Bertot
2018-05-09This version contains an example of using canonical structures soYves Bertot
2018-05-09checkpointYves Bertot
2018-05-09trying to force the resolution of type classes by using a castYves Bertot
2018-05-09an example with type classes, but no class inference triggered yetYves Bertot
2018-05-09repackage with an extra ml file, add a usage of new_type_evarYves Bertot
2018-05-09decompose construction of typed term containing evarsYves Bertot
2018-05-09typoYves Bertot
2018-05-09typoYves Bertot
2018-05-09makefile is necessaryYves Bertot
2018-05-08intermediary stage with an EConstr containing a hand-made evar, fautyYves Bertot
2018-05-08corrects a problem in documenting how to run the demoYves Bertot
2018-05-08problems with bullet listsYves Bertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-23 05:55:29 +0000