| c54deee | SimonBoulier | 29 May 2018, 15:43:55 UTC | Add demo.v to _CoqProjects | 29 May 2018, 15:43:55 UTC |
| 0f575e3 | SimonBoulier | 29 May 2018, 14:14:27 UTC | Fix the rebasing which was totally wrong | 29 May 2018, 14:14:27 UTC |
| 4f5bfe2 | SimonBoulier | 29 May 2018, 12:24:24 UTC | A bit of cleaning | 29 May 2018, 13:37:42 UTC |
| 78aef84 | SimonBoulier | 29 May 2018, 11:54:01 UTC | Comment in movefiles.sh | 29 May 2018, 13:37:42 UTC |
| 7615b00 | SimonBoulier | 29 May 2018, 10:11:11 UTC | Fix movefiles.sh | 29 May 2018, 13:37:42 UTC |
| 7fb9706 | SimonBoulier | 29 May 2018, 10:01:25 UTC | Make translations compile | 29 May 2018, 13:37:42 UTC |
| b862032 | SimonBoulier | 29 May 2018, 09:55:36 UTC | Making the test-suite compile, except evars.v | 29 May 2018, 13:37:42 UTC |
| 51e70da | SimonBoulier | 29 May 2018, 09:29:04 UTC | Remove mli | 29 May 2018, 13:37:42 UTC |
| 3013d08 | SimonBoulier | 29 May 2018, 09:19:04 UTC | Split reify.ml4 in several files | 29 May 2018, 13:37:42 UTC |
| df94b98 | SimonBoulier | 29 May 2018, 07:59:50 UTC | Fix html | 29 May 2018, 13:37:00 UTC |
| 1b1b3a6 | SimonBoulier | 29 May 2018, 07:46:21 UTC | Split is done | 29 May 2018, 13:37:00 UTC |
| 8b9b142 | SimonBoulier | 28 May 2018, 18:28:28 UTC | before copying reify.ml4 | 29 May 2018, 13:37:00 UTC |
| 6857551 | SimonBoulier | 28 May 2018, 14:49:19 UTC | On the road to coq 8.8 | 29 May 2018, 13:34:35 UTC |
| 8ec210f | SimonBoulier | 19 March 2018, 14:57:38 UTC | WIP: trying fixing the extraction | 29 May 2018, 13:33:54 UTC |
| 59cf55d | SimonBoulier | 19 March 2018, 14:56:39 UTC | WIP: trying fixing the extraction | 29 May 2018, 13:33:54 UTC |
| 0c51a2f | SimonBoulier | 19 March 2018, 14:49:44 UTC | UCtx -> UCtxSet | 29 May 2018, 13:30:05 UTC |
| 3c4a9cd | Danil | 16 March 2018, 16:20:51 UTC | Fix depricated functions | 29 May 2018, 13:30:05 UTC |
| 1e60895 | Yannick Forster | 29 May 2018, 13:28:48 UTC | Make automagical merge possible | 29 May 2018, 13:28:48 UTC |
| 40dc8d2 | Danil | 16 March 2018, 14:48:40 UTC | Fix for tmLemma | 29 May 2018, 13:28:10 UTC |
| edd17c4 | Danil | 16 March 2018, 13:24:38 UTC | Using a modifed version of old get_levels. Now it seems to work. | 29 May 2018, 13:28:10 UTC |
| c4781d0 | Danil | 16 March 2018, 10:07:40 UTC | Modifications to make the plugin compatible with Coq 8.8.alpha | 29 May 2018, 13:28:10 UTC |
| 126340f | Yannick Forster | 27 April 2018, 13:59:24 UTC | Better error message for unfold in tmEval | 29 May 2018, 13:13:53 UTC |
| 209d23e | Yannick Forster | 26 April 2018, 15:37:33 UTC | Extended reductionstrategy by unfold option | 29 May 2018, 13:13:44 UTC |
| dd281fc | Théo Winterhalter | 29 May 2018, 09:44:08 UTC | Fix Extraction? | 29 May 2018, 09:44:08 UTC |
| d73d2d3 | Théo Winterhalter | 29 May 2018, 08:27:05 UTC | Change to types_of_case Following @mattam82 | 29 May 2018, 08:27:05 UTC |
| 889b3d1 | SimonBoulier | 28 May 2018, 13:44:26 UTC | Merge pull request #32 from Template-Coq/renameConstraint Rename Constraint to ConstraintSet | 28 May 2018, 13:44:26 UTC |
| ef4a82e | SimonBoulier | 11 May 2018, 17:06:45 UTC | Rename Constraint to ConstraintSet | 11 May 2018, 17:06:45 UTC |
| a81bd81 | Matthieu Sozeau | 02 May 2018, 12:03:38 UTC | Merge pull request #30 from Template-Coq/templatemonad-prop Move TemplateMonad from Prop to Type | 02 May 2018, 12:03:38 UTC |
| 04ad1e0 | SimonBoulier | 30 April 2018, 15:37:23 UTC | Make TemplateMonad going into Type | 02 May 2018, 08:40:29 UTC |
| 433d3bf | SimonBoulier | 02 May 2018, 08:40:11 UTC | Fix make clean | 02 May 2018, 08:40:11 UTC |
| 2d02d18 | SimonBoulier | 30 April 2018, 08:08:05 UTC | make clean should not remove coqdoc.css (this is a hack) | 30 April 2018, 08:08:05 UTC |
| 2932eb2 | nicolas.tabareau | 18 April 2018, 08:18:52 UTC | fix compare_string in univ.v | 18 April 2018, 08:18:52 UTC |
| c2f0215 | nicolas.tabareau | 16 April 2018, 12:22:18 UTC | remove useless case in sort_of_product | 16 April 2018, 12:22:18 UTC |
| 4e86ebf | nicolas.tabareau | 13 April 2018, 15:16:02 UTC | adding impredicativity of Prop | 13 April 2018, 15:16:02 UTC |
| 3310f81 | SimonBoulier | 19 March 2018, 14:57:38 UTC | WIP: trying fixing the extraction | 19 March 2018, 14:57:38 UTC |
| 3c318b4 | SimonBoulier | 19 March 2018, 14:56:39 UTC | WIP: trying fixing the extraction | 19 March 2018, 14:56:39 UTC |
| bff958a | SimonBoulier | 19 March 2018, 14:49:44 UTC | UCtx -> UCtxSet | 19 March 2018, 14:49:44 UTC |
| f0db429 | Danil | 16 March 2018, 16:20:51 UTC | Fix depricated functions | 16 March 2018, 16:20:51 UTC |
| 205aea4 | Danil | 16 March 2018, 14:48:40 UTC | Fix for tmLemma | 16 March 2018, 14:48:40 UTC |
| 2130a8d | Danil | 16 March 2018, 13:24:38 UTC | Using a modifed version of old get_levels. Now it seems to work. | 16 March 2018, 13:24:38 UTC |
| b14fb7c | Danil | 16 March 2018, 10:07:40 UTC | Modifications to make the plugin compatible with Coq 8.8.alpha | 16 March 2018, 10:07:40 UTC |
| aa5b637 | SimonBoulier | 23 February 2018, 10:28:15 UTC | Add castprop.v to the test-suite | 23 February 2018, 10:28:15 UTC |
| 73cde62 | Matthieu Sozeau | 19 February 2018, 16:18:01 UTC | Update README.md with logo | 19 February 2018, 16:18:01 UTC |
| 33529a2 | Matthieu Sozeau | 15 February 2018, 15:10:27 UTC | Backport README and LICENSE changes from master branch | 15 February 2018, 15:16:23 UTC |
| d93f370 | Matthieu Sozeau | 15 February 2018, 15:01:21 UTC | Improve README.md | 15 February 2018, 15:01:21 UTC |
| 26a64e5 | Matthieu Sozeau | 15 February 2018, 14:15:13 UTC | Merge pull request #20 from Template-Coq/remove_cast_type Remove cast_type option, keeping cast_prop. | 15 February 2018, 14:15:13 UTC |
| bb0a9bc | Matthieu Sozeau | 15 February 2018, 13:26:24 UTC | Remove cast_type option, keeping cast_prop. | 15 February 2018, 13:33:33 UTC |
| ce024ed | Matthieu Sozeau | 15 February 2018, 09:02:55 UTC | Merge pull request #18 from SimonBoulier/remove_program Remove program | 15 February 2018, 09:02:55 UTC |
| b8df4df | SimonBoulier | 14 February 2018, 14:44:07 UTC | Fix renaming in add_constructor.v | 14 February 2018, 14:44:07 UTC |
| 31253a3 | SimonBoulier | 10 February 2018, 16:35:58 UTC | Renamming to follow Coq implementation inductive_decl -> one_inductive_body minductive_decl -> mutual_inductive_body constant_decl -> constant_body | 10 February 2018, 16:39:05 UTC |
| 895e2c2 | SimonBoulier | 10 February 2018, 14:38:09 UTC | Remove program | 10 February 2018, 16:39:05 UTC |
| 6f314a0 | SimonBoulier | 10 February 2018, 10:32:48 UTC | Remove debugging msg | 10 February 2018, 15:57:32 UTC |
| f73b32f | SimonBoulier | 10 February 2018, 10:24:33 UTC | Reorganization only | 10 February 2018, 15:57:32 UTC |
| 67d8e71 | SimonBoulier | 10 February 2018, 14:48:57 UTC | Move tsl_param files again (was undo by the PR #11) | 10 February 2018, 15:45:33 UTC |
| 37cbc25 | Matthieu Sozeau | 09 February 2018, 17:58:59 UTC | Put unused BinIntDef dependency (module is copied in BinInt) Avoids a weirdly silent error at install time. | 09 February 2018, 17:59:35 UTC |
| eab7bfd | Matthieu Sozeau | 09 February 2018, 17:53:15 UTC | Translations makefile tweak for coqdoc | 09 February 2018, 17:53:15 UTC |
| b4a9e62 | Matthieu Sozeau | 09 February 2018, 17:52:57 UTC | Makefile dependencies | 09 February 2018, 17:52:57 UTC |
| ba23643 | Matthieu Sozeau | 09 February 2018, 17:52:49 UTC | Fix typo | 09 February 2018, 17:52:49 UTC |
| 3c6f73a | Matthieu Sozeau | 09 February 2018, 17:41:00 UTC | Missing test-suite dependency on the checker | 09 February 2018, 17:41:00 UTC |
| e4ef3ed | Matthieu Sozeau | 09 February 2018, 17:15:46 UTC | Update .gitignore | 09 February 2018, 17:15:46 UTC |
| 4e681fd | Matthieu Sozeau | 09 February 2018, 17:06:37 UTC | Documentation of the main files. Move universe substitution. | 09 February 2018, 17:15:00 UTC |
| 0eb2e23 | Matthieu Sozeau | 09 February 2018, 16:03:21 UTC | html doc fixes | 09 February 2018, 16:03:21 UTC |
| fad1eae | Matthieu Sozeau | 09 February 2018, 15:59:01 UTC | Custom coqdoc.css | 09 February 2018, 15:59:01 UTC |
| e9bd978 | Matthieu Sozeau | 09 February 2018, 15:58:03 UTC | Document theories/Ast.v | 09 February 2018, 15:58:03 UTC |
| fe39ccc | Matthieu Sozeau | 09 February 2018, 15:57:53 UTC | Update README with copyright notice | 09 February 2018, 15:57:53 UTC |
| 959b8d4 | Matthieu Sozeau | 09 February 2018, 15:57:41 UTC | Fix Makefile dependencies | 09 February 2018, 15:57:41 UTC |
| ce1f66f | Matthieu Sozeau | 09 February 2018, 10:43:27 UTC | Move constraint_type inside a module to avoid clashes with comparison. Note it is not the same (Eq|Lt|Le) vs (Eq|Lt|Gt) | 09 February 2018, 10:46:13 UTC |
| 75e0b48 | Matthieu Sozeau | 05 February 2018, 14:47:47 UTC | Merge pull request #11 from aa755/coq-8.7-monad-extraction-pr Functorized the unquote_term function | 05 February 2018, 14:47:47 UTC |
| 35f9408 | Matthieu Sozeau | 05 February 2018, 14:23:58 UTC | split_on_char -> CString.split | 05 February 2018, 14:23:58 UTC |
| 5f39d4a | Matthieu Sozeau | 05 February 2018, 14:16:53 UTC | Fix to compile with camlp4 and 5 | 05 February 2018, 14:16:53 UTC |
| 1eedcf5 | Matthieu Sozeau | 05 February 2018, 14:14:31 UTC | Comment Print Universes in the test-suite | 05 February 2018, 14:14:31 UTC |
| e8e14da | Matthieu Sozeau | 03 February 2018, 14:19:51 UTC | Fixes after rebase on 8.7, everything compiles now, translations included | 05 February 2018, 14:03:52 UTC |
| a7a033c | Abhishek Anand (on Manjaro on brixpro) | 02 February 2018, 03:05:34 UTC | fixed a test case in demo.v. it works | 05 February 2018, 14:03:14 UTC |
| 540b618 | Abhishek Anand (on Manjaro on brixpro) | 02 February 2018, 02:58:40 UTC | implemented inspectTerm. compiles. error in test suite | 05 February 2018, 14:03:14 UTC |
| 17394aa | Abhishek Anand (on Manjaro on brixpro) | 02 February 2018, 00:14:09 UTC | added a print_term to the interface | 05 February 2018, 14:03:14 UTC |
| 8c40df0 | Abhishek Anand (on Manjaro on brixpro) | 02 February 2018, 00:01:26 UTC | everything compiles | 05 February 2018, 14:03:14 UTC |
| bd26348 | Abhishek Anand (on Manjaro on brixpro) | 01 February 2018, 21:19:48 UTC | no error in reify.ml4 | 05 February 2018, 14:03:14 UTC |
| 5f4c569 | Abhishek Anand (on Manjaro on brixpro) | 01 February 2018, 19:27:03 UTC | finished functorizing unquote_term. some errors remain | 05 February 2018, 14:03:14 UTC |
| 8d37a5a | Abhishek Anand (on Manjaro on brixpro) | 01 February 2018, 15:07:33 UTC | WIP: functorizing unquote | 05 February 2018, 14:03:14 UTC |
| 3eaa04e | Abhishek Anand (on Manjaro on brixpro) | 31 January 2018, 19:56:38 UTC | abstracted from_coq_list | 05 February 2018, 14:03:14 UTC |
| e5f7b7c | Abhishek Anand (on Manjaro on brixpro) | 31 January 2018, 00:30:30 UTC | one example of the template_coq impl case | 05 February 2018, 14:03:14 UTC |
| cee23c5 | Abhishek Anand (on Manjaro on brixpro) | 31 January 2018, 00:20:23 UTC | dummy implementations of inspect_Term | 05 February 2018, 14:03:14 UTC |
| 76e8d6f | Abhishek Anand (on Manjaro on brixpro) | 30 January 2018, 23:44:51 UTC | minor changes to get it to compile | 05 February 2018, 14:03:14 UTC |
| d76d38e | Abhishek Anand (on Manjaro on brixpro) | 30 January 2018, 22:48:53 UTC | WIP. adding analysis to the interface | 05 February 2018, 14:03:14 UTC |
| 0ce5966 | Matthieu Sozeau | 04 February 2018, 10:40:02 UTC | Merge pull request #15 from SimonBoulier/bug_is_conv Ah, ah this one annoyed me... | 04 February 2018, 10:40:02 UTC |
| d9c04ce | SimonBoulier | 04 February 2018, 07:46:34 UTC | Fix a bug in is_conv Unfortunately this makes tsl_param not compiling anymore but this is normal | 04 February 2018, 08:14:58 UTC |
| 9a4c6a0 | SimonBoulier | 04 February 2018, 08:10:18 UTC | Fix tsl_param3.v | 04 February 2018, 08:10:18 UTC |
| eb9982b | SimonBoulier | 04 February 2018, 08:04:09 UTC | Move tsl_param files again (was undo by the PR #14) | 04 February 2018, 08:04:09 UTC |
| e4889b3 | Matthieu Sozeau | 03 February 2018, 13:26:54 UTC | Merge pull request #14 from Template-Coq/universe_constraints Universe constraint checking fully working | 03 February 2018, 13:26:54 UTC |
| 6883807 | Matthieu Sozeau | 03 February 2018, 13:07:11 UTC | Forgot one file | 03 February 2018, 13:07:11 UTC |
| d9f2ce3 | Matthieu Sozeau | 03 February 2018, 12:47:08 UTC | Fix universe tests to first try syntactic equality. Everything passes. | 03 February 2018, 13:00:12 UTC |
| f97b923 | Matthieu Sozeau | 03 February 2018, 12:40:36 UTC | Fix dependencies and extraction | 03 February 2018, 13:00:12 UTC |
| 8825cea | Matthieu Sozeau | 03 February 2018, 12:02:39 UTC | Bug fixes | 03 February 2018, 13:00:12 UTC |
| 7f578ef | Matthieu Sozeau | 03 February 2018, 10:12:51 UTC | string_of_term and fix check_eq/check_leq w.r.t. constraints | 03 February 2018, 13:00:12 UTC |
| 8b36555 | SimonBoulier | 03 February 2018, 09:56:40 UTC | fix check_eq_level | 03 February 2018, 13:00:12 UTC |
| 55b7e8e | Matthieu Sozeau | 03 February 2018, 09:47:26 UTC | Fixes in test-suite etc | 03 February 2018, 13:00:12 UTC |
| 4fbe438 | SimonBoulier | 03 February 2018, 09:44:48 UTC | fix in demo.v | 03 February 2018, 13:00:12 UTC |
| 658bed4 | SimonBoulier | 03 February 2018, 09:42:14 UTC | translations compile | 03 February 2018, 13:00:12 UTC |
| 83fc8c9 | Matthieu Sozeau | 02 February 2018, 20:20:14 UTC | Universes in Typing and Checker | 03 February 2018, 13:00:12 UTC |
| dca004e | Matthieu Sozeau | 02 February 2018, 19:08:24 UTC | Quoting of abstract/non-abstract universe contexts | 03 February 2018, 13:00:12 UTC |
