| b1106ec | Matthieu Sozeau | 20 October 2017, 10:33:47 UTC | Update gitignore | 20 October 2017, 10:33:47 UTC |
| 2a328c6 | Matthieu Sozeau | 20 October 2017, 10:33:31 UTC | Add .merlin file | 20 October 2017, 10:33:31 UTC |
| 56dcf88 | Matthieu Sozeau | 20 October 2017, 10:33:09 UTC | Test bug6 reported by Jason in another repo | 20 October 2017, 10:33:09 UTC |
| ac16f4e | Guillaume Claret | 26 November 2015, 18:14:43 UTC | OPAM instructions | 20 October 2017, 10:26:56 UTC |
| f371323 | Gregory Malecha | 16 June 2015, 05:19:50 UTC | bug reports from Jason. | 20 October 2017, 10:25:15 UTC |
| b2555a6 | Matthieu Sozeau | 20 October 2017, 10:17:50 UTC | Merge pull request #42 from SimonBoulier/coq-8.6 Add an example for the denote_term tactic which was undocumented | 20 October 2017, 10:17:50 UTC |
| d244de5 | SimonBoulier | 15 September 2017, 13:36:30 UTC | Add an example for the denote_term tactic which was undocumented | 15 September 2017, 13:37:17 UTC |
| 1dc539f | Matthieu Sozeau | 15 September 2017, 10:26:06 UTC | List.rev bug in quoting of mutual inductives | 15 September 2017, 10:30:32 UTC |
| 32cb5fe | Matthieu Sozeau | 07 September 2017, 13:01:58 UTC | denotation of sorts and constants using an evar_map This creates fresh universes when denoting sorts. | 08 September 2017, 11:20:36 UTC |
| baa3e67 | Matthieu Sozeau | 03 September 2017, 18:51:24 UTC | Reify types of constants and inductives for later manipulation Reify template arities as well | 08 September 2017, 11:20:36 UTC |
| cb519f6 | Matthieu Sozeau | 03 September 2017, 16:13:12 UTC | Quote Proj, CoFix, Metas and Evars properly, removing tUnknown. | 08 September 2017, 11:20:36 UTC |
| 59be0df | Matthieu Sozeau | 05 September 2017, 15:58:24 UTC | Fix TemplateCoqCompiler compilation. | 05 September 2017, 15:58:24 UTC |
| 5fb292f | Matthieu Sozeau | 02 September 2017, 13:16:30 UTC | Fix two bugs in quoting w.r.t. handling mutual inductives. The de Bruijn contexts of mutual inductives and fixpoint prototypes were not reversed properly. | 02 September 2017, 13:16:30 UTC |
| c279ce4 | Matthieu Sozeau | 02 September 2017, 13:15:42 UTC | Output debug information when exceptions are raised while quoting. | 02 September 2017, 13:15:42 UTC |
| f9e3568 | Matthieu Sozeau | 02 September 2017, 11:09:35 UTC | Tail-rec versions of quote_int and quote_string | 02 September 2017, 11:09:35 UTC |
| 88289ef | Matthieu Sozeau | 01 September 2017, 17:06:44 UTC | Update makefile to make always make plugin code | 01 September 2017, 17:06:44 UTC |
| 0880122 | Matthieu Sozeau | 01 September 2017, 16:53:22 UTC | Merge pull request #40 from mattam82/reiftoml Functorized reification and reification to extracted AST | 01 September 2017, 16:53:22 UTC |
| 0fd0ae7 | Matthieu Sozeau | 30 August 2017, 18:21:00 UTC | Functorized reification and reification to extracted AST This PR adds generic support for extracted plugins taking Coq's AST as input, and is used in the CertiCoq project to provide an efficient reification staying entirely in ML. The way this is done is by functorizing the reifier and allowing different quotations types. Two instances are provided, the usual Constr.t quoter which produces a Coq value in the Template.Ast type, and another that quotes into the _extracted_ version of that Ast in ML. The reification code is reused to ensure consistency. For the ML reifier, we slightly tweak extraction to extract strings to char list, improving memory usage and performance significantly. Any extracted plugin wanting to plug to this reifier will have to do the same. | 01 September 2017, 16:51:06 UTC |
| d80d3b1 | Matthieu Sozeau | 10 April 2017, 16:50:46 UTC | Merge branch 'coq-8.5' into coq-8.6 Finish Eval compute in command | 10 April 2017, 16:51:18 UTC |
| ddcf94e | Matthieu Sozeau | 13 December 2016, 14:17:09 UTC | Drastic performance improvement Share string by hashconsing the string objects (reduces memory consumption by half on the Gcd example of certicoq). We do it for whole idents right now, the current Coq string representation does not allow to share prefixes sadly. Also remove the externalisation + elaboration phases when introducing quoted terms, we can bypass it completely and give the term directly for the kernel to check (without bypassing any checks though!). There is still an inefficiency due to retypechecking strings which does not seem so easy to avoid. We went from 240s to 24s when quoting CertiCoq's Gcd example. | 13 February 2017, 23:48:35 UTC |
| db3da94 | Abhishek Anand | 08 December 2016, 03:33:15 UTC | Added the ability to reflect Inductive definitions (#32) * started work on reflecting inductive definitions. Just created a new vernac command "Make Inductive". As of now, it does nothing. Tested the dummy command in demo.v * The command can now declare an empty inductive of a give name. The body is ignored for now. Tested this part in demo.v * documented a bug in unquoting. It incorrectly changes Prop to Set. * preliminary work on transparentification. * Defined kernel's representation of inductive datatypes. * started populating the inductive entries properly. The name and arity are obtained properly populated. However the resultant definition changes arity from Set to Prop. * bugfix : Prop and Set were switched * unable to construct the type of constructors. error. * successfully reflected an inductive type : bool Found the correct input by snooping on the paramcoq plugin (using coq/dev/top_printer.ml) Also, needed to recompile coq so that top_printer.ml gets included in coqtop/coqc: coq/dev$ echo "Top_printer" > printer.mllib then add dev/printer.cma to $CORECMA in coq/Makefile.common * unquoted params, tested mutual and parametrized inductives. * cleaned up the demo * more cleanup for PR * clearnup for PR * removed the unused argument (name) in Make Inductive * exported all members of mutual entry, except universe contexts * properly unquoted mind_entry_record * properly unquoted mind_entry_finite * properly unquoted mind_private * Make Inductive does reduction | 08 December 2016, 03:33:15 UTC |
| 2b239bf | Gregory Malecha | 02 December 2016, 03:37:28 UTC | Merge pull request #31 from yforster/coq-8.6 Coq 8.6 | 02 December 2016, 03:37:28 UTC |
| 2f3fd51 | Yannick Forster | 01 December 2016, 13:55:12 UTC | Finished porting to Coq 8.6, apart from "Quote Definition ... := Eval ... in ..." | 01 December 2016, 13:55:12 UTC |
| 9c90c2f | Yannick Forster | 01 December 2016, 10:38:20 UTC | Fixed tactic quote_term and denote_term | 01 December 2016, 10:38:20 UTC |
| 5771a9d | Yannick Forster | 30 November 2016, 17:57:47 UTC | Started porting to Coq 8.6 | 30 November 2016, 17:57:47 UTC |
| 3eeca69 | Gregory Malecha | 16 November 2016, 21:56:41 UTC | Merge pull request #29 from aa755/pr1 bugfix in unquote_sort: Prop and Set were interchanged. | 16 November 2016, 21:56:41 UTC |
| ce31f27 | Abhishek Anand (@brixpro-home) | 16 November 2016, 18:09:30 UTC | bugfix in unquote_sort: Prop and Set were interchanged. | 16 November 2016, 18:09:30 UTC |
| 59c28b6 | Matthieu Sozeau | 21 October 2016, 08:14:51 UTC | Merge pull request #27 from mattam82/coq-8.5 Fix bug with canonical names | 21 October 2016, 08:14:51 UTC |
| cc827f0 | Matthieu Sozeau | 21 October 2016, 08:11:44 UTC | Add file to test-suite _CoqProject | 21 October 2016, 08:11:44 UTC |
| 524f3d3 | Matthieu Sozeau | 21 October 2016, 08:09:30 UTC | Fix canonical names bug Only reify the canonical versions of constants and turn all constant references into canonical references in the terms. | 21 October 2016, 08:09:30 UTC |
| 2540cb5 | Matthieu Sozeau | 10 August 2016, 15:49:16 UTC | Merge pull request #26 from mattam82/coq-8.5 Change representation of cases, fix denote function | 10 August 2016, 15:49:16 UTC |
| ab3e5fa | Matthieu Sozeau | 10 August 2016, 10:07:42 UTC | Change representation of cases, fix denote function This adds the inductive type on which the case is performed to the case constructors. Fixed the denotation of cases (new info and previous change of repr of branches). | 10 August 2016, 10:07:42 UTC |
| b03e6a2 | Gregory Malecha | 02 May 2016, 16:38:19 UTC | Merge pull request #25 from mattam82/coq-8.5 Fix bugs with LetIn | 02 May 2016, 16:38:19 UTC |
| a177d5f | Matthieu Sozeau | 02 May 2016, 15:34:04 UTC | Change tLetIn order to follow Coq's representation | 02 May 2016, 15:34:04 UTC |
| b8958ae | Matthieu Sozeau | 02 May 2016, 15:06:16 UTC | Fix bugs with LetIn In Coq's representation the body comes first, unlike tLetIn Fixed quote and unquoting as well and added a test in the test-suite. | 02 May 2016, 15:19:08 UTC |
| 8f49839 | Gregory Malecha | 03 April 2016, 19:40:15 UTC | Merge pull request #24 from mattam82/coq-8.5 Fix a bug in casting proofs in Prop | 03 April 2016, 19:40:15 UTC |
| 92c6915 | Matthieu Sozeau | 03 April 2016, 11:19:27 UTC | Fix a bug in casting proofs in Prop It was casting the term with Prop and not its type... Also rework implementation of tagging to be purely functional, passing the in_prop flag along with the environment during reification. Expand test-suite too. | 03 April 2016, 11:19:27 UTC |
| 036cde0 | Gregory Malecha | 14 March 2016, 17:50:40 UTC | bug reported by Randy. | 14 March 2016, 17:50:40 UTC |
| f50447d | Gregory Malecha | 02 March 2016, 00:10:11 UTC | Merge pull request #23 from mattam82/coq-8.5 Add the number of parameters of mutual inductive types in the syntax. | 02 March 2016, 00:10:11 UTC |
| df2bf4c | Matthieu Sozeau | 01 March 2016, 20:44:56 UTC | Add an option to cast maximal subterms of sort Prop Currently done with a reference and repeated retypechecking of subterms, which isn't too bad performance-wise according to P. Letouzey. | 01 March 2016, 20:44:56 UTC |
| 35df610 | Matthieu Sozeau | 01 March 2016, 19:16:55 UTC | Add the number of parameters of mutual inductive types in the syntax. The test-suite goes through unchanged. | 01 March 2016, 19:16:55 UTC |
| de3c4b4 | Gregory Malecha | 09 November 2015, 04:12:20 UTC | fixes to compile with 8.5~beta3 | 09 November 2015, 04:12:47 UTC |
| 76747fc | Gregory Malecha | 18 October 2015, 17:36:58 UTC | Merge pull request #20 from mattam82/coq-8.5 Record the arity of each branch in Case constructs | 18 October 2015, 17:36:58 UTC |
| a7c6980 | Matthieu Sozeau | 18 October 2015, 13:01:42 UTC | Record the arity of each branch in Case constructs (not easily computable otherwise). | 18 October 2015, 13:01:42 UTC |
| c6de18e | Gregory Malecha | 17 July 2015, 05:47:20 UTC | partial denote term tactic from yforester. closes #4 | 17 July 2015, 05:47:20 UTC |
| ac21df4 | Gregory Malecha | 16 July 2015, 04:50:21 UTC | Merge pull request #19 from JasonGross/coq-8.5+ast-in-set Cherry-pick "Put the Ast in [Set] rather than [Type]" into coq-8.5 | 16 July 2015, 04:50:21 UTC |
| e75f3d6 | Jason Gross | 16 June 2015, 11:50:11 UTC | Put the Ast in [Set] rather than [Type] This makes it simpler for the datatype to quote itself without messing around with universes. | 15 July 2015, 23:14:19 UTC |
| fed92ec | Gregory Malecha | 30 June 2015, 17:08:39 UTC | Merge pull request #16 from JasonGross/patch-1 Respect the COQBIN environment variable | 30 June 2015, 17:08:39 UTC |
| 0e54255 | Jason Gross | 30 June 2015, 15:14:47 UTC | Respect the COQBIN environment variable | 30 June 2015, 15:14:47 UTC |
| c071747 | Gregory Malecha | 23 June 2015, 11:27:13 UTC | fixing the bug about parsing non-zero level constrs | 23 June 2015, 11:27:13 UTC |
| 95bf7e5 | Gregory Malecha | 23 June 2015, 11:13:09 UTC | eliminating the old ocamlbuild files. | 23 June 2015, 11:13:09 UTC |
| 9161fd2 | Gregory Malecha | 23 June 2015, 11:08:37 UTC | adding a clean target. | 23 June 2015, 11:08:37 UTC |
| 5bccd89 | Gregory Malecha | 17 June 2015, 22:16:22 UTC | reify types of axioms. (closes #9) - this does not handle polymorphic constants. | 17 June 2015, 22:16:22 UTC |
| 54d2b46 | Gregory Malecha | 17 June 2015, 21:50:51 UTC | fixing reduce bug. | 17 June 2015, 21:50:51 UTC |
| 5254a9e | Gregory Malecha | 17 June 2015, 21:26:41 UTC | Merge pull request #15 from mattam82/coq-8.5 Use the arity information of constructors | 17 June 2015, 21:26:41 UTC |
| 59e3cf7 | Matthieu Sozeau | 17 June 2015, 16:09:17 UTC | Use the arity information of constructors that comes from the kernel (not used by the kernel itself though, only the normalized arity is, mind_nf_lc). | 17 June 2015, 16:09:17 UTC |
| 22a5c0b | Gregory Malecha | 15 June 2015, 22:04:47 UTC | fixing the Makefile. closes bug #8 | 15 June 2015, 22:05:08 UTC |
| c636911 | Maxime Dénès | 07 June 2015, 11:16:21 UTC | Fix DECLARE PLUGIN statement. Was required to make tactic quote_term work. | 07 June 2015, 11:16:21 UTC |
| 9c6dd83 | Maxime Dénès | 27 May 2015, 14:31:28 UTC | Port to Coq 8.5. | 27 May 2015, 14:31:28 UTC |
| 3798874 | Gregory Malecha | 01 April 2015, 01:56:17 UTC | hnf reduction in types of constructors. | 14 April 2015, 21:02:46 UTC |
| 4dd2b24 | Gregory Malecha | 01 April 2015, 01:53:16 UTC | another bug report? | 14 April 2015, 21:02:46 UTC |
| e3a9a8d | Gregory Malecha | 15 October 2014, 21:24:24 UTC | Adding the number of parameters to tCase | 15 October 2014, 21:24:24 UTC |
| 0860495 | Gregory Malecha | 08 October 2014, 17:29:36 UTC | the all-important LICENSE. | 08 October 2014, 17:29:36 UTC |
| a9d98b3 | Gregory Malecha | 08 October 2014, 17:19:53 UTC | Fix the order of branches in match expressions. | 08 October 2014, 17:19:53 UTC |
| 93127d5 | Gregory Malecha | 23 September 2014, 18:27:55 UTC | fixing some of the build scripts. | 23 September 2014, 18:27:55 UTC |
| 68792fd | Gregory Malecha | 23 September 2014, 18:22:07 UTC | remove some warnings. | 23 September 2014, 18:22:07 UTC |
| f89cf47 | Gregory Malecha | 23 September 2014, 18:19:09 UTC | reify really opaque things. | 23 September 2014, 18:19:09 UTC |
| 89c47fd | Gregory Malecha | 22 September 2014, 23:08:48 UTC | adding support of reification of opaque symbols. | 22 September 2014, 23:08:48 UTC |
| 66f7246 | Gregory Malecha | 18 September 2014, 00:39:47 UTC | support for inductive types. | 18 September 2014, 00:39:47 UTC |
| 7ca4024 | Gregory Malecha | 12 September 2014, 22:30:27 UTC | bug fix, don't support quoting in sections. | 12 September 2014, 22:31:04 UTC |
| 1d0aade | Gregory Malecha | 05 September 2014, 00:02:13 UTC | fixing the Makefile in test-suite. | 05 September 2014, 00:02:13 UTC |
| 56ee4f3 | Gregory Malecha | 04 September 2014, 23:04:56 UTC | bug fix for multiple reification. | 04 September 2014, 23:04:56 UTC |
| f0c1996 | Gregory Malecha | 03 September 2014, 21:41:12 UTC | don't fail on reification of universes | 03 September 2014, 21:41:12 UTC |
| e3beba8 | Gregory Malecha | 03 September 2014, 20:04:10 UTC | also do plus in the demo. | 03 September 2014, 20:04:10 UTC |
| 6e0c6fb | Gregory Malecha | 03 September 2014, 20:00:41 UTC | support for recursive reification. | 03 September 2014, 20:00:41 UTC |
| 37f7120 | Gregory Malecha | 05 August 2014, 16:01:31 UTC | fix the quoting of set and prop. | 05 August 2014, 16:01:31 UTC |
| 3e6580c | Gregory Malecha | 29 July 2014, 22:09:05 UTC | Update README.md use a bit more markup. | 29 July 2014, 22:09:05 UTC |
| 2f6b463 | Gregory Malecha | 29 July 2014, 22:06:56 UTC | Updated README.md | 29 July 2014, 22:06:56 UTC |
| 44a40ab | Gregory Malecha | 29 July 2014, 22:03:09 UTC | Adding a Makefile for the demo. | 29 July 2014, 22:03:09 UTC |
| 1c8eaa6 | Gregory Malecha | 14 July 2014, 07:56:06 UTC | buggy support for Make - A better way to do it is likely to go through phases of elaboration. - This allows me to add holes to the Make syntax. | 14 July 2014, 07:56:06 UTC |
| 3d864fe | Gregory Malecha | 12 July 2014, 14:42:06 UTC | Create README.md | 12 July 2014, 14:42:06 UTC |
| 862b4dd | Gregory Malecha | 11 July 2014, 20:02:31 UTC | support for fixpoints. | 11 July 2014, 20:02:31 UTC |
| 0df8f5a | Gregory Malecha | 11 July 2014, 19:16:24 UTC | now with suppport for running evaluation functions | 11 July 2014, 19:17:38 UTC |
| aac7fd3 | Gregory Malecha | 11 July 2014, 13:40:53 UTC | handling for case. - patterns do not exist in Coq's core representation - I need a way to get constructor names (in their order) | 11 July 2014, 13:40:53 UTC |
| e416e34 | Gregory Malecha | 11 July 2014, 04:43:53 UTC | an alternative style to building definitions. | 11 July 2014, 04:43:53 UTC |
| 8beb4a8 | Gregory Malecha | 11 July 2014, 04:20:35 UTC | a few bug fixes + building syntax. | 11 July 2014, 04:20:35 UTC |
| 223120a | Gregory Malecha | 09 July 2014, 20:17:01 UTC | a few missing files. | 09 July 2014, 20:17:01 UTC |
| 07cdac8 | Gregory Malecha | 09 July 2014, 20:12:52 UTC | the ability to reify simple terms. | 09 July 2014, 20:12:52 UTC |
| a199a10 | Gregory Malecha | 09 July 2014, 02:54:12 UTC | working on a quoting plugin. | 09 July 2014, 02:54:12 UTC |
