aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Simplifying the code of Tacinterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
| |
| * Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq ↵Gravatar Pierre Letouzey2016-05-04
| |\ | | | | | | | | | into v8.5
| * | Fixing subst.out after changing spacing in goal output (24a125b77).Gravatar Hugo Herbelin2016-05-04
| | |
| * | Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Haskell extraction code would allow line-wrapping of the Haskell type definition, which would lead to unparseable Haskell code when the linebreak occured just before the type name. In particular, with a term name of 46 characters or more, the following Coq code: Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt. Extraction Language Haskell. Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx. would produce: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :: Unit xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx = Tt which failed to compile with GHC (according to Haskell's indentation rules, the "Unit" line must be indented to be treated as a continuation of the previous line). This patch always forces the type onto a separate line, and ensures that it is always indented by 2 spaces (just like the body of each definition).
| * | Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | | | | | | | | Note that extracting terms containing primitive projections is still utterly broken, so don't use them.
| * | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
| | | | | | | | | | | | Patch by Matthieu, Enrico and myself.
* | | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into ↵Gravatar Pierre Letouzey2016-05-04
|\ \ \ | | | | | | | | | | | | trunk
| | * | Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | | | | | | | | | A single terminal character can take up to 5 bytes, e.g. "''^A'".
| | * | In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
| | * | Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | | | | | | | | | | | | | We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time.
| | * | Fix bug #3825: Universe annotations on notations should pass through or be ↵Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | | | | | | | | | rejected.
| | * | Test file for #4695: Slow Qed.Gravatar Maxime Dénès2016-05-03
| | | |
| | * | Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
| | | |
| | * | Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
| | | | | | | | | | | | | | | | Disclaimer: I have no idea what I am doing.
* | | | A note concerning the "Drop" command.Gravatar Matej Kosik2016-05-03
| | | |
| | * | Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
| | | |
* | | | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.Gravatar Matej Kosik2016-05-03
| | | |
| | * | Call hooks when terminating a definition proof (bug #4663).Gravatar Guillaume Melquiond2016-05-03
| | | | | | | | | | | | | | | | Also register properly the kind of definition.
| | * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
| | | |
| | * | Make votour a bit more robust/forgiving with respect to user commands (bug ↵Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | | | | | #4702).
| | * | Properly handle notations containing spaces (bug #4538).Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a notation was starting or ending a space, Coq assumed the notation had no terminal symbol in either places. Coq also considered a notation containing only spaces to be productive. As stated in the documentation, extraneous spaces are only meant as printing hints, they are not meant to have any influence on parsing.
| | * | Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When encountering a "simpl nomatch" constant, the reduction machinery tries to unfold it. If the subsequent partial reduction does not produce any match construct, it keeps going from the reduced term. Unfortunately, the reduced term has been refolded in the meantime, which means that some of the previous reduction steps have been canceled, thus causing an infinite loop. This patch delays the refolding till the very end, so that reduction always progresses. Disclaimer: I have no idea what I am doing here. The patch compiles the standard library and the test suite properly, so hopefully they contain enough tests to exercise the reduction machinery.
* | | | Generate parsing rules for ML tactics in the same order as before a7917a32.Gravatar Pierre-Marie Pédrot2016-05-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Once again showing the fragility of the parsing engine, commit a7917a32 reversed the relative order of the declaration of parsing rules for tactics declared through TACTIC EXTEND. There is probably no good order at all, but for retrocompatibility, this patch enforces the original one.
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\ \ \ \ | | |/ / | |/| |
* | | | Useless code in Tacentries.Gravatar Pierre-Marie Pédrot2016-05-02
| | | |
| * | | Reduce ide/coq.png to 256x256.Gravatar Guillaume Melquiond2016-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Commit 1774a87 increased the file to 1024x1024. This had two adverse consequences. First, the icon was too large to be used as a window icon ("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had an icon at runtime. Second, the file was also used in the About message box, which was thus exceeding the display size of any reasonably-priced device. This commit reverts the file to a saner size (still larger than the original 66x100 picture).
| * | | Fix incorrect cbv reduction of primitive projections. (Bug #4634)Gravatar Guillaume Melquiond2016-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As noticed by Cyprien Mangin, projected terms cannot directly be used as head values. Indeed, they might be applications (e.g. constructors as in the bug report) whose arguments would thus be missing from the evaluation stack when doing any iota-reduction step. The only case where it would make sense is when the evaluation stack is empty, as an optimization. Indeed, in that case, the arguments are put on the stack, and then immediately put back inside the term.
| * | | Make the language grammar much more precise. (Fix bugs #4682 and #4683)Gravatar Guillaume Melquiond2016-04-28
| | | | | | | | | | | | | | | | | | | | | | | | Rather than being isolated words, commands and tactics now extend till dot separators. So bullets can be defined as living only at the top level of proofs, which should make their detection much more robust.
| * | | Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
| | | |
| * | | Fix missing newline in coqchk engagement (bug #4694).Gravatar Guillaume Melquiond2016-04-28
| | | |
| * | | An example for cd139311e, showing a consequence of not convertingGravatar Hugo Herbelin2016-04-28
| | | | | | | | | | | | | | | | | | | | constants up to their canonical name (taken from Daniel's formalization of Puiseux theorem).
* | | | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
* | | | Revert "Not taking arguments given by name or position into account when"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
* | | | Revert "Adding a target for beautification."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695.
* | | | Revert "Adding a target check-beautify for testing reparsability of"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
* | | | Revert "So as to beautify to work, do not use notations in Inductive types"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
* | | | Revert "Protect the beautifier from change in the lexer state (typically by"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
* | | | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5.
* | | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* | | | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
* | | | Revert "Temporary deactivate re-interpretation of terms in beautify."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
* | | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* | | | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
* | | | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | the levels." This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:49:47 +0000