aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\
* \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \
* \ \ Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \
* | | | Declaring ltac plugin, so that static linking works.Gravatar Hugo Herbelin2017-04-01
| | | |
| * | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
| * | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | RawLocal -> CLocal
| * | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | This is a bit long, but it is to keep a symmetry with constr_expr.
| * | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ / /
* | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \
| * \ \ Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| |\ \ \
| | | * | Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately.
| | | * | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
| * | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
* | | | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This prevents Coq from unfolding IZR in ring_simplify and field_simplify. This is a change of behavior for users of morphism rings, so they might have to pass the postprocess option to Add Ring/Field if they want morphisms to be automatically expanded. There are two predefined morphisms in the standard library: IDphi (when polynomial coefficients have the same type as constants) and gen_phiZ (when the only available constants are 0 and 1). They are hardcoded as transparent.
* | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
* | | | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bang indicates an argument that must be reduced, a star indicates an argument that must be handled recursively. PEeval: R r0 r1 add mul sub opp C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8! 9 10! 11 12* 13! FEeval: R r0 r1 add mul sub opp div inv C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8 9 10! 11 12! 13 14* 15! Pphi_dev: R r0 r1 add mul sub opp C c0 c1 ceq phi sign varmap pol 0 1 2 3 4 5 6 7 8! 9! 10! 11! 12! 13* 14! Pphi_pow: R r0 r1 add mul sub opp C c0 c1 ceq phi Cpow powphi pow sign varmap pol 0 1 2 3 4 5 6 7 8! 9! 10! 11! 12 13! 14 15! 16* 17! display_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi sign varmap num den 0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13! 14* 15! 16! display_pow_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi Cpow powphi pow sign varmap num den 0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13 14! 15 16! 17* 18! 19! PCond: R r0 r1 add mul sub opp eq C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8 9! 10 11! 12 13* 14!
* | | | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
| |_|/ / |/| | |
| | * | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| |/ / | | | | | | | | | | | | | | | Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372) "Anomaly: Not a valid information when defining mutual fixpoints that are not mutual with Function".
* | | [extraction] Flush formatters at end of output.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | Previous implementations of `Pp` flushed on newline, however, depending on the formatter this may not be always the case. We now alwayas flush the formatters before closing the file as this is the intended behavior.
* | | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`.
* | | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent.
* | | [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | We replace open/close box commands in favor of the create box ones.
* | | [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* | | [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* | | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags.
* | | [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone.
* | | Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\ \ \
* \ \ \ Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
|\ \ \ \
* \ \ \ \ Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\ \ \ \ \
* | | | | | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
| | | * | | [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | | | | | | | No functional change.
| | | * | | [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | No functional change, one extra copy introduced but it seems hard to avoid.
| | * | | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| |/ / / |/| | | | | | | | | | | | | | | | | | | Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
* | | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
|\ \ \ \
* | | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
| | | | | | | | | | | | | | | | | | | | The constant was useless after 9f56baf which fixed #5073.
| | | | * Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|_|/ |/| | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
| | | * [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
| | | | | | | | | | | | | | | | This is needed to fix `Declare ML Module "ltac_plugin".
* | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
|\ \ \ \ | | | | | | | | | | | | | | | Tactic Notation
| | | * | TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
* | | | Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
| | | | | | | | | | | | | | | | | | | | This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
|\ \ \ \ | | |_|/ | |/| |
* | | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* | | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
| | | * [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| |_|/ |/| |
* | | Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \
* | | | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
* | | | Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
| | | |
* | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:11:51 +0000