| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-07 | Merge pull request #15 from ejgallego/add_travis | Yves Bertot | |
| [travis] Add Travis File. | |||
| 2018-11-06 | Merge pull request #14 from ppedrot/coqpp-port | Emilio Jesús Gallego Arias | |
| Port to coqpp. | |||
| 2018-11-06 | [travis] Add Travis File. | Emilio Jesus Gallego Arias | |
| We only test dev for master. | |||
| 2018-11-05 | Port to coqpp. | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge pull request #12 from SkySkimmer/command-atts | Yves Bertot | |
| Fix for coq/coq#8515 (command driven attributes) | |||
| 2018-11-02 | Fix for coq/coq#8515 (command driven attributes) | Gaëtan Gilbert | |
| 2018-10-31 | Revert "Merge pull request #13 from ↵ | Yves Bertot | |
| herbelin/master+adapt-coq8718-declaration-hooks" This reverts commit 9e8d0b077d8021e468ec0bc117438695c0b243bf, reversing changes made to 56c3ae6296994cc288d4931110118617bb5bb978. | |||
| 2018-10-30 | Merge pull request #13 from herbelin/master+adapt-coq8718-declaration-hooks | Yves Bertot | |
| Adapting to Coq PR #8718: declare_definition now takes a UState.t + using new predefined no_hook | |||
| 2018-10-30 | Adapting to Coq PR #8718: declare_definition now takes a UState.t. | Hugo Herbelin | |
| Also use new predefined Lemmas.no_kook. | |||
| 2018-10-29 | Merge pull request #10 from mattam82/pr8671-fix | Yves Bertot | |
| PR 8671: Remove store / goal extra argument | |||
| 2018-10-26 | PR 8671: Remove store / goal extra argument | Matthieu Sozeau | |
| 2018-10-22 | Merge pull request #11 from ejgallego/vernac+monify_hook | Yves Bertot | |
| [coq] Adapt for PR #8704. | |||
| 2018-10-11 | [coq] Adapt for PR #8704. | Emilio Jesus Gallego Arias | |
| 2018-10-01 | fix deprecation warnings | Yves Bertot | |
| 2018-10-01 | adapts to master on Oct. 1st 2018, but warnings remain | Yves Bertot | |
| 2018-07-18 | the same license as for the coq development | Yves Bertot | |
| 2018-05-30 | Merge branch 'remove_constr_of_global' | Yves Bertot | |
| 2018-05-30 | remove warnings and merge printing function for econstr terms | Yves Bertot | |
| 2018-05-30 | remove uses of Universes.constr_of_global | Yves Bertot | |
| 2018-05-30 | this version has no warnings when compiling | Yves Bertot | |
| 2018-05-30 | Merge pull request #6 from maximedenes/fix-printer | Yves Bertot | |
| Use user printer for terms instead of debug printer | |||
| 2018-05-28 | Use user printer for terms instead of debug printer | Maxime Dénès | |
| 2018-05-17 | Merge pull request #5 from gares/fix/tuto2 | Yves Bertot | |
| [tuto2] Clarify where the name of the ML plugin is used | |||
| 2018-05-17 | Merge pull request #4 from gares/fix/tuto0 | Yves Bertot | |
| fix plugin name in tuto0 | |||
| 2018-05-17 | Merge pull request #3 from gares/patch-1 | Yves Bertot | |
| Add some setup instructions | |||
| 2018-05-17 | [tuto2] Clarify where the name of the ML plugin is used | Enrico Tassi | |
| 2018-05-17 | add little test | Enrico Tassi | |
| - tests the plugin can actually be loaded (eg with the wrong DECLARE PLUGIN it loads but then the tactic is not in scope) - sine is listed in _CoqProject one can open it with CoqIDE/PG and get the -I -R flags from the _CoqProject automatically | |||
| 2018-05-17 | DECLARE PLUGIN "$name" === Declare ML Module "$name" | Enrico Tassi | |
| 2018-05-17 | Add some setup instructions | Enrico | |
| 2018-05-17 | Merge pull request #2 from gares/gares-patch-1 | Yves Bertot | |
| [tuto1] Minor fixes to comments | |||
| 2018-05-17 | [tuto1] Minor fixes to comments | Enrico | |
| 2018-05-12 | adds a hello world tactic in tuto0 | Yves Bertot | |
| 2018-05-11 | Updates the contents of the third tutorial | Yves Bertot | |
| 2018-05-11 | This version contains documentation for the code of the packing tactic | Yves Bertot | |
| warning have been removed Examples for the use of type classes and canonical structures in automatic proof have been moved to the end. | |||
| 2018-05-11 | Adds a tactic that hides the contents of an hypothesis from view | Yves Bertot | |
| 2018-05-11 | Use the more colloquial EConstr.t type instead of EConstr.constr | Yves Bertot | |
| 2018-05-10 | This version has type inference performing proofs, using both type classes | Yves Bertot | |
| and canonical structures | |||
| 2018-05-10 | finished the example where type class resolution is forced | Yves Bertot | |
| 2018-05-09 | This version contains an example of using canonical structures so | Yves Bertot | |
| that type-checking actually triggers the automatic build of a proof. | |||
| 2018-05-09 | checkpoint | Yves Bertot | |
| 2018-05-09 | trying to force the resolution of type classes by using a cast | Yves Bertot | |
| 2018-05-09 | an example with type classes, but no class inference triggered yet | Yves Bertot | |
| 2018-05-09 | repackage with an extra ml file, add a usage of new_type_evar | Yves Bertot | |
| 2018-05-09 | decompose construction of typed term containing evars | Yves Bertot | |
| 2018-05-09 | typo | Yves Bertot | |
| 2018-05-09 | typo | Yves Bertot | |
| 2018-05-09 | makefile is necessary | Yves Bertot | |
| 2018-05-08 | intermediary stage with an EConstr containing a hand-made evar, fauty | Yves Bertot | |
| 2018-05-08 | corrects a problem in documenting how to run the demo | Yves Bertot | |
| 2018-05-08 | problems with bullet lists | Yves Bertot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |