aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-06-16
| | | | | | | | with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
|
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-06-16
| | | | presence of entries starting with a non-terminal such as "b ^2".
* Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-06-16
|
* Fixing printing of inversion as.Gravatar Hugo Herbelin2016-06-16
|
* Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-06-16
|
* Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-06-16
|
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
|
* In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-06-16
|
* Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-06-16
| | | | implicit is found whether one writes (sig P) or {x|P x}.
* Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-06-16
| | | | implicit arguments when in beautification mode.
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
| | | | | | simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* Changing rule for "*" in Operator_Properties so that, iterated, itGravatar Hugo Herbelin2016-06-16
| | | | does not print to ** which is a keyword.
* Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-06-16
| | | | | calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module").
* Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
| | | | | | | | | | computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available. For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _", the same way as if we had said: Arguments eq_refl {A} {x}.
* Merge '/pr/206' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge PR #195: Complete is_* family of term-examining tactics.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* \ \ Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \ \
* \ \ \ Merge PR #211: Fix a printing typo in LtacProf.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \ \
* \ \ \ \ Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #100: fresh now accepts more things than just identifiers.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \ \ \ \
* | | | | | | Fix Makefile after ssrmatching mergeGravatar Enrico Tassi2016-06-16
| | | | | | |
* | | | | | | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What one needs to know in 3rd party makefiles, like plugins ones, is the Coq version and the OCaml version number. This option prints the 2 values on a single line separated by spaces. The already existing --version outputs the same piece of info but in a format meant for user consumption, and hence harder to parse.
* | | | | | | ideslave: do not bail out in case of XML errorGravatar Enrico Tassi2016-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Used to be an `exit 1`, now an error message is printed on stderr. This helps people experimenting with the XML protocol.
* | | | | | | Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
| | | | | | |
| | | | | * | Update CHANGESGravatar Jason Gross2016-06-16
| | | | | | |
| | | | | * | Add is_constGravatar Jason Gross2016-06-16
| | | | | | |
* | | | | | | Merge branch 'pr/146' into trunkGravatar Enrico Tassi2016-06-16
|\ \ \ \ \ \ \
| * | | | | | | Ignore generated .ml file for ssrmatchingGravatar Enrico Tassi2016-06-16
| | | | | | | |
* | | | | | | | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \ \ \ \ \ \ \
| | | | | * | | | Fix another missing newlineGravatar Jason Gross2016-06-16
| | | | | | | | |
| | | | | * | | | Fix a printing typoGravatar Jason Gross2016-06-16
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | Introduced by b21fefc0ec0aab2560d0b654f1a1f4203898388b
| | | | * | | | Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a stupid fix that only allows to take into account the change in memory layout. The check will simply fail when encountering a unguarded inductive or (co)fixpoint.
| | | | * | | | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
* | | | | | | | Fix test-suite for opened bug #4813.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | |
| | | | * | | | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper.
| | * | | | | | ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
| | * | | | | | Merge branch 'pr/146' into trunkGravatar Enrico Tassi2016-06-15
| |/| | | | | | |/| | | | | | |
| | * | | | | | ssrmatching: simple test for Ltac APIGravatar Enrico Tassi2016-06-15
| | | | | | | |
| | * | | | | | ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
| | | | | | | |
| | * | | | | | ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
| | | | | | | |
| | * | | | | | Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | for uniformity with other Debug options.
* | | | | | | | typographyGravatar Matej Kosik2016-06-15
| | | | | | | |
* | | | | | | | ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpackGravatar Pierre Letouzey2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends already on all the .cmx inside it, no need to state explicitely that the .cmxs depends on these inner .cmx. Same thing concerning .cmxs built out of a single .cmx.
* | | | | | | | Makefile.build: ensure a build failure in case of a missing ruleGravatar Pierre Letouzey2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Earlier (as in #4812), a target with some declared dependencies (e.g. in a .d) but no building rule would lead to a successful build, even though it is actually incomplete. Side effect: it is now mandatory to declare phony targets in a .PHONY statement.
* | | | | | | | fix test-suite/ide Makefile (stupid typo)Gravatar Enrico Tassi2016-06-15
| | | | | | | |
| | | | * | | | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | | | | | | Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In pre 8.6, `Pp` provided its own reimplementation of `Pervasives.flush_all`, with different semantics. Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of points were silently switched to the `Pervasives` version, which may lead to some subtle printing differences. As a preventive measure, we restore the same semantics for these parts of the codebase. Note that we don't re-introduce Coq's `flush_all` for several reasons: - Consumers of the logging API should not mess with flushing and Formatters as this is backend dependent (i.e: when in IDEs). Use of `Format` should be fully encapsulated if we want some hope of IDEs taking full control. - As used, the old semantics of `flush_all` were fragile.
* | | | | | | | Fix for bug #4784Gravatar Emilio Jesus Gallego Arias2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We revert the change of flushing strategy in the toplevel. PR #179 introduced a different flushing in toplevel, but it creates problems as new lines appear when Set Printing Width is large and proof general complains, see bugzilla#4784. The use of `flush_all` also produces missing output. IMO, this is a pitfall of the current setup, in particular, `Format` is used without enclosing expressions in top-level boxes, as required. This results in undefined behavior and fragile printing such as this bug exemplifies. Test suite passes.
* | | | | | | | Repair the build of ide/coqidetop.cmxs (fix #4812)Gravatar Pierre Letouzey2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Restore the .cmxa-->.cmxs rule from the Makefile. Sorry, I was thinking that all plugins would now be built from .mlpack (hence using only the .cmx-->.cmxs rule), and I forgot about this coqidetop business. Now the really intersting question is : why on earth 'make world' was silently failing to build this file but succeeding nonetheless ?!
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:27:27 +0000