| c81ffca | Matthieu Sozeau | 08 August 2018, 10:19:20 UTC | Merge pull request #25 from Template-Coq/wcbveval Weak call-by-value evaluation definition | 08 August 2018, 10:19:20 UTC |
| aa2a2c4 | Gregory Malecha | 25 July 2018, 16:45:14 UTC | remove the dependency of TemplateMonad on monad_utils - monad_utils comtains a partial monad library, it should be replaced will a full-featured monad library (in another package). in the meantime, this allows users to import only the core TemplateMonad and not pull in the monad_utils dependency. | 27 July 2018, 14:47:43 UTC |
| 1ea1a8f | Matthieu Sozeau | 27 July 2018, 13:14:25 UTC | Fix evaluation of TBox: it should reduce to itself when applied | 27 July 2018, 13:14:25 UTC |
| c864bc3 | Matthieu Sozeau | 26 July 2018, 13:03:49 UTC | Rename Extraction to TemplateExtraction | 26 July 2018, 14:24:01 UTC |
| 5900f1b | Matthieu Sozeau | 20 July 2018, 12:17:06 UTC | Merge pull request #63 from yforster/intactics Run template programs in tactics | 20 July 2018, 12:17:06 UTC |
| 010820a | Yannick Forster | 19 July 2018, 17:02:26 UTC | Added failing test as well | 19 July 2018, 17:02:26 UTC |
| c18d75f | Yannick Forster | 19 July 2018, 16:59:16 UTC | Run template programs in tactics | 19 July 2018, 16:59:16 UTC |
| 428baa4 | nicolas tabareau | 18 July 2018, 08:59:27 UTC | Merge pull request #62 from TheoWinterhalter/type-in-type-fix Type in type fix | 18 July 2018, 08:59:27 UTC |
| fb63f5a | Théo Winterhalter | 18 July 2018, 07:22:58 UTC | Add type_in_type to the library of configs | 18 July 2018, 07:22:58 UTC |
| b3058b1 | Théo Winterhalter | 18 July 2018, 07:19:10 UTC | Add checker_flags as an argument to eq_universe | 18 July 2018, 07:19:21 UTC |
| 19e57fd | Matthieu Sozeau | 17 July 2018, 15:29:24 UTC | Move Erase to Extract, more appropriate naming | 17 July 2018, 15:29:24 UTC |
| dcc1df4 | Matthieu Sozeau | 17 July 2018, 15:26:34 UTC | Fix wcbvEval use of mkApps | 17 July 2018, 15:26:34 UTC |
| c5f18db | Matthieu Sozeau | 05 July 2018, 09:04:39 UTC | Add extraction makefile | 17 July 2018, 15:20:34 UTC |
| b28243e | Matthieu Sozeau | 04 July 2018, 22:06:05 UTC | Erasure of global context and conjecture | 17 July 2018, 15:20:34 UTC |
| 5e74d00 | Matthieu Sozeau | 04 July 2018, 21:22:07 UTC | Move erasure to its own directory | 17 July 2018, 15:20:34 UTC |
| cc6e1f4 | Matthieu Sozeau | 04 July 2018, 21:10:05 UTC | More erasure | 17 July 2018, 15:20:34 UTC |
| 28d88cb | Matthieu Sozeau | 03 May 2018, 09:56:58 UTC | Erasure theorems Fix substitution and wcbveval after R. Pollack's comments. Added a term wf judgment Substitution now uses [mkApps] in the [tApp] case to ensure preservation of the representation invariant on applications, specified as [Ast.wf]. The lemma [subst_mkApps] shows that [mkApps] and substitution properly commute. Most substitution and lifting lemmas hold for non-wellformed terms also, only a few require a well-formedness property. | 17 July 2018, 15:20:34 UTC |
| e80290e | Matthieu Sozeau | 23 April 2018, 16:27:35 UTC | Add a few tests for erasure | 17 July 2018, 15:20:34 UTC |
| fd695b3 | Matthieu Sozeau | 23 April 2018, 16:15:48 UTC | First try at erasure correctness conjecture | 17 July 2018, 15:20:34 UTC |
| 4a963ba | Matthieu Sozeau | 19 April 2018, 15:44:57 UTC | Add Erasure module formalizing the extraction's erasure | 17 July 2018, 15:20:34 UTC |
| fb4b58d | Matthieu Sozeau | 19 April 2018, 15:44:30 UTC | Add sort_of to Retyping | 17 July 2018, 15:20:34 UTC |
| 849c88d | Matthieu Sozeau | 19 April 2018, 15:24:46 UTC | Fix monad operation definitions to be usable in nested recursive calls | 17 July 2018, 15:20:34 UTC |
| b347951 | Matthieu Sozeau | 19 April 2018, 15:04:32 UTC | Add Retyping module with fast type inference algorithm | 17 July 2018, 15:20:34 UTC |
| 05317fd | Matthieu Sozeau | 18 April 2018, 15:22:50 UTC | Add a spec of weak call-by-value evaluation | 17 July 2018, 15:20:34 UTC |
| 190faa8 | Matthieu Sozeau | 18 April 2018, 15:22:09 UTC | Add a MetaTheory file with conjectures of the main metatheoretical properties | 17 July 2018, 15:20:34 UTC |
| 5fa0bff | Matthieu Sozeau | 17 July 2018, 15:19:45 UTC | Treat tCoFix and tProj in checker reduction correctly | 17 July 2018, 15:19:45 UTC |
| c6e6b47 | Matthieu Sozeau | 17 July 2018, 15:13:37 UTC | Use checker_flags more consistently, remove universe todos in Typing | 17 July 2018, 15:13:37 UTC |
| 71e17bf | Matthieu Sozeau | 17 July 2018, 14:57:59 UTC | Add cofixpoint reduction rules. Some congruences may be missing still | 17 July 2018, 14:57:59 UTC |
| d9ca1db | Matthieu Sozeau | 18 April 2018, 14:12:12 UTC | Add primitive projections to parallel reduction | 17 July 2018, 14:29:10 UTC |
| c381f51 | SimonBoulier | 04 July 2018, 14:06:40 UTC | Use better reduction functions | 05 July 2018, 07:28:15 UTC |
| 0e45003 | SimonBoulier | 05 July 2018, 06:49:18 UTC | Small change in denote_reduction_strategy | 05 July 2018, 06:49:18 UTC |
| ec4a68d | Matthieu Sozeau | 04 July 2018, 16:09:32 UTC | Add missing closed issues files to test-suite | 04 July 2018, 16:10:17 UTC |
| 5a47961 | Matthieu Sozeau | 04 July 2018, 16:02:33 UTC | Merge pull request #57 from gmalecha/TemplateMonad-in-Prop Make TemplateMonad Universe Polymorphic (and move it to its own module) | 04 July 2018, 16:02:33 UTC |
| 6c39c58 | Matthieu Sozeau | 04 July 2018, 15:11:55 UTC | Fix typing issue, make Monad polymorphic and TemplateProgram cumulative to avoid universe inconsistencies. | 04 July 2018, 15:54:30 UTC |
| 3289d17 | Gregory Malecha | 25 June 2018, 15:06:10 UTC | addressing the universe problems? | 04 July 2018, 15:53:18 UTC |
| 0834b21 | Gregory Malecha | 25 June 2018, 14:29:07 UTC | fixing the build. | 04 July 2018, 15:51:40 UTC |
| 3f570cd | Gregory Malecha | 23 June 2018, 18:05:27 UTC | making TemplateMonad universe polymorphic. | 04 July 2018, 15:51:40 UTC |
| bba61f3 | Gregory Malecha | 23 June 2018, 15:38:16 UTC | splitting the TemplateMonad into another file. | 04 July 2018, 15:49:08 UTC |
| 6cd8ab7 | Gregory Malecha | 23 June 2018, 14:46:31 UTC | if TemplateMonad is in Type, then there are universe problems - An alternative would be to make it universe polymorphic. | 04 July 2018, 15:44:05 UTC |
| e983579 | Matthieu Sozeau | 04 July 2018, 15:41:39 UTC | Merge pull request #44 from yforster/tmInferInstance Implemented tmInferInstance | 04 July 2018, 15:41:39 UTC |
| 3a487fc | Yannick Forster | 04 July 2018, 15:34:38 UTC | Fixed deprecated errors, added test to CoqProject | 04 July 2018, 15:34:38 UTC |
| cbae883 | Yannick Forster | 04 July 2018, 15:33:20 UTC | Merge branch 'tmInferInstance' of https://github.com/yforster/template-coq into tmInferInstance | 04 July 2018, 15:33:20 UTC |
| 9108e7c | Yannick Forster | 30 May 2018, 14:52:02 UTC | Implemented tmInferInstance | 04 July 2018, 15:32:00 UTC |
| a0945be | Matthieu Sozeau | 04 July 2018, 15:30:33 UTC | Merge pull request #40 from yforster/tmEvalUnfold Add unfold to reductionStrategy to tmEval | 04 July 2018, 15:30:33 UTC |
| f802ded | Yannick Forster | 04 July 2018, 15:29:14 UTC | Error message for ill-typed terms in tmUnquote (#39) * Extended reductionstrategy by unfold option * Better error message for unfold in tmEval * Quoting inside sections now works * tmUnquote throws error for ill-typed terms * Revert "Quoting inside sections now works" This reverts commit 15b1cf8d777904c4e1a007ba10c91e3fcb95beb3. * Revert "Better error message for unfold in tmEval" This reverts commit 6958808d0ceb3a910ed44a107ee0dd7063700766. * Revert "Extended reductionstrategy by unfold option" This reverts commit 5255e196fde3ce02ee035e503c4aeca41a29fa07. * Right parens for try-catch * Extended reductionstrategy by unfold option * Fixed syntax error | 04 July 2018, 15:29:14 UTC |
| 8dca765 | Yannick Forster | 30 May 2018, 15:37:02 UTC | Added test-case for tmInferInstance | 04 July 2018, 15:29:10 UTC |
| 4576a71 | Yannick Forster | 30 May 2018, 14:52:02 UTC | Implemented tmInferInstance | 04 July 2018, 15:28:43 UTC |
| 1ce2ab8 | Matthieu Sozeau | 04 July 2018, 15:25:40 UTC | Merge pull request #43 from yforster/implement-tmExistingInstance Implement tmExistingInstance | 04 July 2018, 15:25:40 UTC |
| 4968db6 | Yannick Forster | 04 July 2018, 15:09:52 UTC | Merge branch 'tmInferInstance' of https://github.com/yforster/template-coq into tmInferInstance | 04 July 2018, 15:09:52 UTC |
| e42c1b7 | Yannick Forster | 30 May 2018, 15:37:02 UTC | Added test-case for tmInferInstance | 04 July 2018, 15:08:46 UTC |
| f094249 | Yannick Forster | 30 May 2018, 14:52:02 UTC | Implemented tmInferInstance | 04 July 2018, 15:08:27 UTC |
| c948e97 | Yannick Forster | 04 July 2018, 15:02:24 UTC | Merge branch 'implement-tmExistingInstance' of https://github.com/yforster/template-coq into implement-tmExistingInstance | 04 July 2018, 15:02:24 UTC |
| c46f1e8 | Yannick Forster | 30 May 2018, 12:51:10 UTC | Test for failing tmExistingInstance | 04 July 2018, 15:01:33 UTC |
| daee2e3 | Yannick Forster | 30 May 2018, 12:49:06 UTC | Add test | 04 July 2018, 15:01:33 UTC |
| 84d78ad | Yannick Forster | 30 May 2018, 12:43:03 UTC | Implemented tmExistingInstance | 04 July 2018, 15:00:55 UTC |
| c6e5021 | Yannick Forster | 04 July 2018, 14:48:47 UTC | Merge branch 'tmEvalUnfold' of https://github.com/yforster/template-coq into tmEvalUnfold | 04 July 2018, 14:48:47 UTC |
| 5b19235 | Yannick Forster | 04 July 2018, 14:48:15 UTC | Added test case for unfolding | 04 July 2018, 14:48:15 UTC |
| 0114825 | Yannick Forster | 04 July 2018, 14:47:56 UTC | Right way to get evaluable_global_reference | 04 July 2018, 14:47:56 UTC |
| ed10dc3 | Yannick Forster | 26 April 2018, 15:37:33 UTC | Extended reductionstrategy by unfold option | 04 July 2018, 13:54:01 UTC |
| 1638ebe | Matthieu Sozeau | 03 July 2018, 13:34:13 UTC | Fix translations w.r.t. checker_flags | 03 July 2018, 13:35:53 UTC |
| 905b935 | Matthieu Sozeau | 26 June 2018, 12:57:57 UTC | Merge pull request #54 from TheoWinterhalter/univcheck88 Add configuration class, possibility to disable check_leq | 26 June 2018, 12:57:57 UTC |
| b31c5ad | SimonBoulier | 20 June 2018, 14:04:21 UTC | Fix a bug in tmLemma | 21 June 2018, 08:51:37 UTC |
| d5ead2d | SimonBoulier | 20 June 2018, 14:00:45 UTC | Hack to fix the extraction issue. | 21 June 2018, 08:51:27 UTC |
| 4c1885a | Matthieu Sozeau | 14 June 2018, 16:31:50 UTC | Fix makefiles so that install works. It's a HACK | 14 June 2018, 16:31:50 UTC |
| ec18a6f | Matthieu Sozeau | 14 June 2018, 13:31:22 UTC | Merge pull request #56 from TheoWinterhalter/loadpath Fix #55 (make install and logical path) | 14 June 2018, 13:31:22 UTC |
| 33a1954 | Théo Winterhalter | 08 June 2018, 09:05:55 UTC | Fix #55 (make install and logical path) | 08 June 2018, 09:05:55 UTC |
| 6c4d25e | Théo Winterhalter | 07 June 2018, 12:59:07 UTC | Use default config to avoid stack overflow in test-suite | 07 June 2018, 12:59:07 UTC |
| 58dd982 | Théo Winterhalter | 06 June 2018, 14:17:47 UTC | Fix checker extraction | 06 June 2018, 14:17:47 UTC |
| a61cd64 | Théo Winterhalter | 06 June 2018, 14:12:19 UTC | Propagating checker_flags | 06 June 2018, 14:12:19 UTC |
| 3c17ca4 | Théo Winterhalter | 06 June 2018, 09:47:08 UTC | Apply config to the correct function | 06 June 2018, 09:50:10 UTC |
| 0d34dac | Théo Winterhalter | 06 June 2018, 09:23:50 UTC | Add config class (and option to disable universe checking) | 06 June 2018, 09:50:10 UTC |
| 8c241e1 | SimonBoulier | 06 June 2018, 06:13:29 UTC | Merge remote-tracking branch 'loic-p/map_constr_with_binders' into coq-8.8 | 06 June 2018, 06:13:29 UTC |
| 812e42a | Matthieu Sozeau | 05 June 2018, 15:18:51 UTC | One more typo fix | 05 June 2018, 15:18:51 UTC |
| 154998f | Matthieu Sozeau | 05 June 2018, 15:16:05 UTC | Merge branch 'comment-cleanup' of https://github.com/gmalecha/template-coq into gmalecha-comment-cleanup | 05 June 2018, 15:16:05 UTC |
| cb391cc | loic-p | 05 June 2018, 14:58:38 UTC | Fix case tLetin in function map_constr_with_binders | 05 June 2018, 14:58:38 UTC |
| aa8d3e2 | SimonBoulier | 05 June 2018, 14:48:23 UTC | Fix backporting | 05 June 2018, 14:48:23 UTC |
| 63d8794 | SimonBoulier | 05 June 2018, 12:37:55 UTC | Merge branch 'backport_88' into coq-8.8 | 05 June 2018, 12:37:55 UTC |
| a11266d | SimonBoulier | 04 June 2018, 08:15:38 UTC | Backporting to Coq 8.8.0 | 04 June 2018, 08:15:38 UTC |
| 4774efb | SimonBoulier | 31 May 2018, 07:57:29 UTC | Make Template Check able to check a term (and not only a reference). Note that Template Check still cannot typecheck a not typable term because of pretyping. To allow it we would need a function glob_constr -> constr which don't pretype. | 02 June 2018, 13:10:41 UTC |
| d04179a | SimonBoulier | 01 June 2018, 19:03:23 UTC | Fix evar bug in test-suite. | 01 June 2018, 19:04:15 UTC |
| 93c6d86 | SimonBoulier | 01 June 2018, 17:41:37 UTC | Fix string_of_term. | 01 June 2018, 18:32:44 UTC |
| 5dd6fb2 | SimonBoulier | 01 June 2018, 17:11:04 UTC | Remove some warnings. | 01 June 2018, 17:11:04 UTC |
| b853398 | SimonBoulier | 01 June 2018, 17:10:53 UTC | Fix a bug in conversion checker. | 01 June 2018, 17:10:53 UTC |
| 19e3ed3 | SimonBoulier | 01 June 2018, 16:39:52 UTC | Handle universe polymorphism when running tmDefinition or tmLemma. | 01 June 2018, 16:39:52 UTC |
| b2e6d08 | Matthieu Sozeau | 31 May 2018, 08:04:32 UTC | More fixes to travis instructions to update opam | 31 May 2018, 08:04:32 UTC |
| 8f4b8d6 | Matthieu Sozeau | 31 May 2018, 07:59:47 UTC | Update COQ_VER for this branch: using released package coq.8.8.0 | 31 May 2018, 07:59:47 UTC |
| 2b7e873 | Gregory Malecha | 30 May 2018, 17:37:56 UTC | a typo in the typo-correction. | 30 May 2018, 17:37:56 UTC |
| 80408df | Gregory Malecha | 30 May 2018, 17:13:07 UTC | clean up some comments in Ast.v | 30 May 2018, 17:13:07 UTC |
| 46dbd25 | Yannick Forster | 30 May 2018, 15:37:02 UTC | Added test-case for tmInferInstance | 30 May 2018, 15:37:02 UTC |
| 8154565 | Yannick Forster | 30 May 2018, 15:20:18 UTC | Fixed None in tmInferInstance | 30 May 2018, 15:20:36 UTC |
| 4c701ae | Yannick Forster | 30 May 2018, 14:52:02 UTC | Implemented tmInferInstance | 30 May 2018, 14:56:09 UTC |
| 27e8c91 | Yannick Forster | 30 May 2018, 12:51:10 UTC | Test for failing tmExistingInstance | 30 May 2018, 12:51:10 UTC |
| d898b20 | Yannick Forster | 30 May 2018, 12:49:06 UTC | Add test | 30 May 2018, 12:49:06 UTC |
| d9696d6 | Yannick Forster | 30 May 2018, 12:48:16 UTC | Remove Vernac | 30 May 2018, 12:48:16 UTC |
| e6bb391 | Yannick Forster | 30 May 2018, 12:47:49 UTC | Remove commented code | 30 May 2018, 12:47:49 UTC |
| 252e3b1 | Yannick Forster | 30 May 2018, 12:43:03 UTC | Implemented tmExistingInstance | 30 May 2018, 12:46:40 UTC |
| e37d8b6 | SimonBoulier | 29 May 2018, 22:36:13 UTC | Better output for Template Check | 29 May 2018, 22:36:13 UTC |
| b7d9059 | SimonBoulier | 29 May 2018, 16:17:53 UTC | Trying to fix travis | 29 May 2018, 16:17:53 UTC |
| 616632f | SimonBoulier | 29 May 2018, 16:05:54 UTC | Add test for universes | 29 May 2018, 16:05:54 UTC |
| e87a521 | SimonBoulier | 29 May 2018, 16:05:31 UTC | Set travis for coq-trunk branch | 29 May 2018, 16:05:31 UTC |
