| bacd547 | Gregory Malecha | 07 June 2019, 18:24:24 UTC | adding `Generate Definition` and use for generating definitions. | 07 June 2019, 18:24:24 UTC |
| 0f1a439 | Gregory Malecha | 15 May 2019, 17:43:52 UTC | signal errors more aggressively | 15 May 2019, 17:43:52 UTC |
| ca90338 | Gregory Malecha | 15 May 2019, 13:42:31 UTC | porting the last function. | 15 May 2019, 13:42:31 UTC |
| cb3630b | Gregory Malecha | 02 May 2019, 14:57:39 UTC | proposal for a port of translation_utils.v | 14 May 2019, 13:12:26 UTC |
| 8827e89 | SimonBoulier | 14 May 2019, 10:29:23 UTC | remove some warnings | 14 May 2019, 10:29:23 UTC |
| 3efe206 | SimonBoulier | 14 May 2019, 10:13:57 UTC | Logic -> Logic0 | 14 May 2019, 10:13:57 UTC |
| dd55375 | Gregory Malecha | 13 May 2019, 13:23:43 UTC | fixing a dependency | 13 May 2019, 13:23:43 UTC |
| 7b89e55 | Gregory Malecha | 13 May 2019, 13:18:30 UTC | Merge remote-tracking branch 'origin/coq-8.8' into plugin-tm-interp-rebase | 13 May 2019, 13:18:30 UTC |
| 298efe7 | Gregory Malecha | 13 May 2019, 12:28:54 UTC | moving plugin-demo to test-suite | 13 May 2019, 12:28:54 UTC |
| 0c53aee | SimonBoulier | 13 May 2019, 08:09:50 UTC | Correct type of definitions produced by Make Definition | 13 May 2019, 08:56:44 UTC |
| 85ff767 | SimonBoulier | 13 May 2019, 08:08:51 UTC | Reintroduce tmDefinitionRed and tmAxiomRed Partly revert 38e9c3ba3637e847bf03a0bbe87c5c8504ee17df | 13 May 2019, 08:56:44 UTC |
| 7be3585 | SimonBoulier | 10 May 2019, 11:04:25 UTC | Correct (un)quoting of universes and test suite | 13 May 2019, 07:25:06 UTC |
| 03002e1 | SimonBoulier | 09 May 2019, 18:14:13 UTC | Bit of cleaning | 13 May 2019, 07:25:06 UTC |
| 368ec02 | SimonBoulier | 09 May 2019, 17:34:21 UTC | make everything compiling | 13 May 2019, 07:25:06 UTC |
| c93b247 | SimonBoulier | 29 April 2019, 12:09:33 UTC | Take polymorphic universes in account | 13 May 2019, 07:25:06 UTC |
| 44af14b | SimonBoulier | 29 April 2019, 08:50:39 UTC | Change the specification of universe managment | 13 May 2019, 07:25:06 UTC |
| cdf3b07 | Gregory Malecha | 10 May 2019, 06:59:09 UTC | fixing all the broken builds. | 10 May 2019, 06:59:09 UTC |
| 1f9d6ed | Gregory Malecha | 25 April 2019, 11:42:27 UTC | type annotation. | 10 May 2019, 05:59:26 UTC |
| d16c4f6 | Gregory Malecha | 24 April 2019, 22:03:50 UTC | updating the extraction makefile. | 10 May 2019, 05:59:26 UTC |
| 6d47f3b | Gregory Malecha | 24 April 2019, 17:45:27 UTC | removing some debug printing. | 10 May 2019, 05:59:26 UTC |
| 5f1d46a | Gregory Malecha | 24 April 2019, 17:43:20 UTC | cleanup the implementation of genLens | 10 May 2019, 05:59:26 UTC |
| 436ad8b | Gregory Malecha | 24 April 2019, 17:32:48 UTC | working gen-lens | 10 May 2019, 05:59:26 UTC |
| 9cff86c | Gregory Malecha | 24 April 2019, 16:43:07 UTC | some bug fixes. | 10 May 2019, 05:59:26 UTC |
| ff4c5c6 | Abhishek Anand (optiplex7010@home) | 24 April 2019, 14:24:46 UTC | put the segfault generator in Gallina now. so just make should trigger it, instead of needing to manually edit the extract | 10 May 2019, 05:59:26 UTC |
| 78943fb | Abhishek Anand (optiplex7010@home) | 24 April 2019, 05:10:46 UTC | again segfault, with: let cl2s cl = String.concat "" (List.map (String.make 1) cl) let getFields mi = match mi.ind_bodies with | [] -> Printf.printf "no ind bodies\n"; None | oib :: l -> print_string (String.concat "in get fields: " [cl2s (oib.ind_name)]); (match l with | [] -> (match oib.ind_ctors with | [] -> Printf.printf "no constructors\n"; None | ctor0 :: l0 -> (match l0 with | [] -> Some { coq_type = oib.ind_name; ctor = (let (p, _) = ctor0 in let (x0, _) = p in x0); fields = oib.ind_projs } | _ :: _ -> None)) | _ :: _ -> Printf.printf "multiple constructors\n"; None) Most likely, the inductive structure is corrupt. Some use of Obj.magic is likely suspect. | 10 May 2019, 05:59:26 UTC |
| db909fe | Abhishek Anand (optiplex7010@home) | 24 April 2019, 04:29:43 UTC | manually added prints in the extract of getFields: let getFields mi = Printf.printf "in get fields\n"; match mi.ind_bodies with | [] -> Printf.printf "no ind bodies\n"; None | oib :: l -> (match l with | [] -> (match oib.ind_ctors with | [] -> Printf.printf "no constructors\n"; None | ctor0 :: l0 -> (match l0 with | [] -> Some { coq_type = oib.ind_name; ctor = (let (p, _) = ctor0 in let (x0, _) = p in x0); fields = oib.ind_projs } | _ :: _ -> None)) | _ :: _ -> Printf.printf "multiple constructors\n"; None) it turns out there are multiple constructors for the Point record. | 10 May 2019, 05:59:26 UTC |
| 5a41c83 | Gregory Malecha | 24 April 2019, 02:21:45 UTC | trying something to fix the import problem in pcuic | 10 May 2019, 05:59:26 UTC |
| 72f4f93 | Gregory Malecha | 24 April 2019, 02:21:25 UTC | removing unused imports. | 10 May 2019, 05:59:24 UTC |
| ec2408e | Abhishek Anand (optiplex7010@home) | 24 April 2019, 03:30:40 UTC | it seems that tmQuoteInductiveR succeeds and getFields fails | 10 May 2019, 05:59:07 UTC |
| 695b53e | Abhishek Anand (optiplex7010@home) | 24 April 2019, 00:21:44 UTC | genLensN returns the error "failed to get info" | 10 May 2019, 05:59:07 UTC |
| 385d597 | Gregory Malecha | 15 April 2019, 02:13:18 UTC | unneeded import. | 10 May 2019, 05:59:07 UTC |
| 7cd2ce5 | Gregory Malecha | 15 April 2019, 02:04:05 UTC | some more Makefile fixes. | 10 May 2019, 05:59:07 UTC |
| 7ba0c2d | Gregory Malecha | 14 April 2019, 20:17:14 UTC | toying with Makefile rules. | 10 May 2019, 05:59:07 UTC |
| a9cc30f | Gregory Malecha | 14 April 2019, 19:18:15 UTC | bug fixes for extraction. | 10 May 2019, 05:59:04 UTC |
| 35aadf1 | Gregory Malecha | 10 April 2019, 18:04:06 UTC | some debugging. | 10 May 2019, 05:55:04 UTC |
| 1843a97 | Abhishek Anand (optiplex7010@home) | 10 April 2019, 13:52:24 UTC | now showoff just does tmDefinition. Not_found error | 10 May 2019, 05:55:04 UTC |
| ad2d42b | Abhishek Anand (optiplex7010@home) | 10 April 2019, 04:45:46 UTC | just quoting constant segfaults | 10 May 2019, 05:55:03 UTC |
| a57a9fc | Abhishek Anand (optiplex7010@home) | 10 April 2019, 04:44:25 UTC | just quoting and printing segfaults | 10 May 2019, 05:55:03 UTC |
| 7503ef0 | Abhishek Anand (optiplex7010@home) | 10 April 2019, 04:09:39 UTC | the error seems to happen in the extracted code. will simplify | 10 May 2019, 05:55:03 UTC |
| 2c01af5 | Abhishek Anand (optiplex7010@home) | 10 April 2019, 03:58:35 UTC | ran the lens example, it segfaulted | 10 May 2019, 05:55:03 UTC |
| a8f9af2 | Abhishek Anand (optiplex7010@home) | 10 April 2019, 00:51:24 UTC | cleaned up the lens example to not require other libs. removed admits as they would make Demo.v crash with "admitted axiom" | 10 May 2019, 05:55:03 UTC |
| 1140ce3 | Abhishek Anand (optiplex7010@home) | 10 April 2019, 00:30:01 UTC | ported genLensN to TM.Extractable | 10 May 2019, 05:55:03 UTC |
| f222f44 | Gregory Malecha | 10 April 2019, 00:10:10 UTC | fixing some Makefiles | 10 May 2019, 05:55:03 UTC |
| 7027bd3 | Gregory Malecha | 09 April 2019, 23:55:54 UTC | fixing the checker plugin | 10 May 2019, 05:55:02 UTC |
| f0664a5 | Gregory Malecha | 09 April 2019, 22:55:35 UTC | a simple README for the plugin-demo | 10 May 2019, 05:53:58 UTC |
| 0e60700 | Gregory Malecha | 09 April 2019, 22:29:45 UTC | some fixes | 10 May 2019, 05:53:58 UTC |
| 6b6039d | Abhishek Anand (optiplex7010@home) | 09 April 2019, 22:25:23 UTC | removed the redundant to-lower. it is now done in template-coq/gen-src | 10 May 2019, 05:53:58 UTC |
| a90e46c | Abhishek Anand (optiplex7010@home) | 09 April 2019, 22:15:13 UTC | propagated the renaming in HEAD^ to other files. eg. Common -> Common0 | 10 May 2019, 05:53:55 UTC |
| b7e1507 | Abhishek Anand (optiplex7010@home) | 09 April 2019, 21:54:03 UTC | removed more name clashes by blacklisting. error remains: CAMLOPT -pp -c -for-pack Demo_plugin src/g_demo_plugin.ml4 File "_none_", line 1: Error: Unbound module Run_extractable | 10 May 2019, 05:52:59 UTC |
| 2142297 | Abhishek Anand (optiplex7010@home) | 09 April 2019, 21:44:39 UTC | capitalization fix. need to run to-lower before copying from template-coq | 10 May 2019, 05:52:59 UTC |
| 3590abe | Gregory Malecha | 09 April 2019, 21:05:11 UTC | lift clean_name and split_name | 10 May 2019, 05:52:59 UTC |
| 7b68979 | Gregory Malecha | 09 April 2019, 21:00:16 UTC | working build of demo-plugin. | 10 May 2019, 05:52:59 UTC |
| 4f89f7e | Gregory Malecha | 09 April 2019, 20:30:54 UTC | everything seems to work except the linker is droppign a symbol | 10 May 2019, 05:52:59 UTC |
| aa77ea2 | Gregory Malecha | 09 April 2019, 19:43:31 UTC | now template-coq builds | 10 May 2019, 05:52:56 UTC |
| 4201e97 | Abhishek Anand (on lenovo laptop) | 09 April 2019, 23:02:37 UTC | partial implementation of to_kernname. can now test quoting | 10 May 2019, 05:50:02 UTC |
| edca396 | Abhishek Anand (on lenovo laptop) | 09 April 2019, 16:57:26 UTC | implemented to_constr_ev and unquote reduction strategy | 10 May 2019, 05:50:02 UTC |
| 6162e3f | Abhishek Anand (on lenovo laptop) | 09 April 2019, 15:58:18 UTC | implemented Ast_denoter.unquote_universe_instance | 10 May 2019, 05:50:02 UTC |
| 6b7b15a | Gregory Malecha | 09 April 2019, 14:33:43 UTC | a plugin that works! | 10 May 2019, 05:50:02 UTC |
| a160bdf | Gregory Malecha | 09 April 2019, 14:13:50 UTC | making the template-coq directory compile. | 10 May 2019, 05:49:46 UTC |
| 80dabe1 | Abhishek Anand (on lenovo laptop) | 09 April 2019, 05:03:54 UTC | added a second phase compilation/mlpack for extraction-based plugin make in `template-coq` fully compiles make in `checker` fails | 10 May 2019, 05:49:22 UTC |
| 6348d59 | Gregory Malecha | 09 April 2019, 01:59:39 UTC | an almost working plugin | 10 May 2019, 05:49:22 UTC |
| 37dfc33 | Abhishek Anand (on lenovo laptop) | 09 April 2019, 01:26:29 UTC | some fixes for compilation | 10 May 2019, 05:49:22 UTC |
| affec44 | Abhishek Anand (on lenovo laptop) | 09 April 2019, 00:58:41 UTC | implemented all of denoter instance except unquote univ instance Ast_quoter had unquote functions too: all of them except unquote univ instance. | 10 May 2019, 05:49:22 UTC |
| 2531523 | Gregory Malecha | 09 April 2019, 00:58:17 UTC | get rid of the gen-src directory | 10 May 2019, 05:49:22 UTC |
| 36c8d2d | Gregory Malecha | 08 April 2019, 23:49:42 UTC | things should now compile. | 10 May 2019, 05:49:22 UTC |
| 0a93f77 | Gregory Malecha | 08 April 2019, 22:58:31 UTC | support for ConstantEntry | 10 May 2019, 05:49:16 UTC |
| 49c6a57 | Gregory Malecha | 08 April 2019, 22:40:34 UTC | implementation of `of_mib` | 10 May 2019, 05:49:16 UTC |
| 55f18ee | Abhishek Anand (on lenovo laptop) | 08 April 2019, 23:57:12 UTC | implemented inspect_term | 10 May 2019, 05:49:16 UTC |
| e6d346f | Abhishek Anand (on lenovo laptop) | 08 April 2019, 23:04:25 UTC | WIP:Extraction denoter instance. compiles, but many items are failwith | 10 May 2019, 05:49:14 UTC |
| 6c864ce | Gregory Malecha | 08 April 2019, 21:40:22 UTC | implementing a few more pieces of run_extractable. | 10 May 2019, 05:48:48 UTC |
| 41e5016 | Abhishek Anand (on lenovo laptop) | 08 April 2019, 22:16:04 UTC | reducde code duplication | 10 May 2019, 05:48:48 UTC |
| 5823791 | Abhishek Anand (on lenovo laptop) | 08 April 2019, 22:02:12 UTC | fixed the compiler error in denote_term. provided instance of Denoter for running live in Coq | 10 May 2019, 05:48:41 UTC |
| a9c2850 | Abhishek Anand (on lenovo laptop) | 08 April 2019, 20:19:15 UTC | fixed many compilation errors. 1 remains: File "src/denote.ml", line 1: Error: The implementation src/denote.ml does not match the interface src/denote.cmi: The value `denote_term' is required but not provided | 10 May 2019, 05:48:00 UTC |
| cbd3ad3 | Abhishek Anand (on lenovo laptop) | 08 April 2019, 20:04:33 UTC | denote_term function now has no errors. there is another error: Error: The implementation src/denote.ml does not match the interface src/denote.cmi: The value `denote_term' is required but not provided The value `map_evm' is required but not provided The value `unquote_universe_instance' is required but not provided The value `unquote_level' is required but not provided The value `unquote_string' is required but not provided The value `unquote_ident' is required but not provided The value `unquote_bool' is required but not provided The value `unquote_list' is required but not provided The value `unquote_pair' is required but not provided Makefile.coq:604: recipe for target 'src/denote.cmx' failed | 10 May 2019, 05:47:20 UTC |
| c50a009 | Gregory Malecha | 08 April 2019, 17:18:56 UTC | looking at functorizing denote hacky rules to build the plugin. | 10 May 2019, 05:46:17 UTC |
| da004a6 | Abhishek Anand (on lenovo laptop) | 08 April 2019, 04:07:07 UTC | did rel, var, and cast cases of to_constr. WIP: universes. | 10 May 2019, 04:50:01 UTC |
| 737d32e | Gregory Malecha | 05 April 2019, 03:07:29 UTC | fixing run_extractable. - the previous implementation was completely wrong. | 10 May 2019, 04:50:01 UTC |
| 77b3c77 | Gregory Malecha | 05 April 2019, 02:18:08 UTC | checkpoint. giving up on trying to do native extraction. | 10 May 2019, 04:50:01 UTC |
| 85878a3 | Gregory Malecha | 01 April 2019, 03:43:12 UTC | working on plugin extraction | 10 May 2019, 04:49:52 UTC |
| d408169 | SimonBoulier | 09 May 2019, 18:14:13 UTC | Bit of cleaning | 09 May 2019, 18:14:13 UTC |
| 2e6fdd2 | SimonBoulier | 09 May 2019, 17:34:21 UTC | make everything compiling | 09 May 2019, 17:34:21 UTC |
| 4295c7e | SimonBoulier | 29 April 2019, 12:09:33 UTC | Take polymorphic universes in account | 29 April 2019, 12:09:33 UTC |
| 7b475a8 | SimonBoulier | 29 April 2019, 08:50:39 UTC | Change the specification of universe managment | 29 April 2019, 08:53:05 UTC |
| 7c2ca91 | SimonBoulier | 25 April 2019, 10:08:53 UTC | Remove tmDefinitionRed, tmLemmaRed, tmAxiomRed | 29 April 2019, 08:51:59 UTC |
| e377141 | SimonBoulier | 25 April 2019, 09:21:16 UTC | Add .mli file | 29 April 2019, 08:51:59 UTC |
| 247b1ce | SimonBoulier | 12 April 2019, 10:17:42 UTC | Remove tmMkDefinition but it introduce a universe bug | 29 April 2019, 08:51:59 UTC |
| cf79152 | SimonBoulier | 11 April 2019, 15:08:32 UTC | Define commands of Template Coq (Test Quote, Make Definition, ...) as TemplateMonad programs | 29 April 2019, 08:51:59 UTC |
| dc8203a | SimonBoulier | 25 April 2019, 09:02:07 UTC | typos | 25 April 2019, 09:02:11 UTC |
| 1439571 | Théo Winterhalter | 18 April 2019, 14:35:36 UTC | Slight update of the proof of red1_pred1, still incomplete | 25 April 2019, 08:59:50 UTC |
| e442f95 | Théo Winterhalter | 18 April 2019, 14:11:22 UTC | Fix compiling | 25 April 2019, 08:59:50 UTC |
| 38c01b2 | Théo Winterhalter | 18 April 2019, 12:30:38 UTC | Fix cofix unfolding which was swapping return branch and scrutinee | 25 April 2019, 08:59:50 UTC |
| 470d0c7 | Yann Régis Gianas | 15 April 2019, 10:52:20 UTC | Fix typo | 15 April 2019, 13:09:58 UTC |
| 040a61f | SimonBoulier | 14 April 2019, 07:13:21 UTC | Fix patches of PCUIC, sorry for having broken the build | 14 April 2019, 07:32:08 UTC |
| 3f77f4c | SimonBoulier | 11 April 2019, 09:07:23 UTC | Remove Meta variables tMeta from everywhere. Fix #81 | 12 April 2019, 10:27:51 UTC |
| 5e7faa0 | SimonBoulier | 12 April 2019, 10:26:51 UTC | Fix Extraction | 12 April 2019, 10:26:51 UTC |
| ef3bfb0 | Yannick Forster | 11 April 2019, 10:08:25 UTC | Merge pull request #122 from MetaCoq/tmEval_kn Allow qualified names in unfold reduction strategy. Fix #65 | 11 April 2019, 10:08:25 UTC |
| ec9bda2 | SimonBoulier | 11 April 2019, 08:36:22 UTC | Allow qualified names in unfold reduction strategy. Fix #65 | 11 April 2019, 08:36:22 UTC |
| 74f5fc5 | Matthieu Sozeau | 09 April 2019, 14:14:10 UTC | Cleanup in confluence and SR. Not finished for cofix/fix | 10 April 2019, 08:19:09 UTC |
| 1904c4f | Matthieu Sozeau | 07 April 2019, 14:12:00 UTC | Confluence for CoFix up to a lifting lemma | 10 April 2019, 08:19:09 UTC |
| 7d1455d | Matthieu Sozeau | 06 April 2019, 22:26:24 UTC | Improve lemma statement | 10 April 2019, 08:19:09 UTC |
