aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-06-16Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-06-16Simplification in ppvernac.ml.Hugo Herbelin
2016-06-16Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
No other changes (long only because of a change of indentation).
2016-06-16Fixing extra space in printing bullets.Hugo Herbelin
2016-06-16Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
Fixing : in Declare Module.
2016-06-16Fixing printing of Instance.Hugo Herbelin
2016-06-16Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-06-16Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-06-16Fixing printing of Arguments.Hugo Herbelin
2016-06-16Printing notations as parsed.Hugo Herbelin
2016-06-16So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
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.
2016-06-16Fixing missing substitution / printing cases of TacSelect.Pierre-Marie Pédrot
2016-06-16Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
presence of entries starting with a non-terminal such as "b ^2".
2016-06-16Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-06-16Fixing printing of inversion as.Hugo Herbelin
2016-06-16Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-06-16Fixing printing of induction/destruct as.Hugo Herbelin
2016-06-16Fixing printing of pat%constr.Hugo Herbelin
2016-06-16In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-06-16Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
implicit is found whether one writes (sig P) or {x|P x}.
2016-06-16Being defensive in printing implicit arguments also with manualHugo Herbelin
implicit arguments when in beautification mode.
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-06-16Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
does not print to ** which is a keyword.
2016-06-16Protect the beautifier from change in the lexer state (typically byHugo Herbelin
calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module").
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
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}.
2016-06-16Merge '/pr/206' into trunkEnrico Tassi
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge PR #211: Fix a printing typo in LtacProf.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Merge PR #100: fresh now accepts more things than just identifiers.Pierre-Marie Pédrot
2016-06-16Fix Makefile after ssrmatching mergeEnrico Tassi
2016-06-16--print-version produces machine readable version infoEnrico Tassi
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.
2016-06-16ideslave: do not bail out in case of XML errorEnrico Tassi
Used to be an `exit 1`, now an error message is printed on stderr. This helps people experimenting with the XML protocol.
2016-06-16Remove inappropriate comment.Maxime Dénès
2016-06-16Update CHANGESJason Gross
2016-06-16Add is_constJason Gross
2016-06-16Merge branch 'pr/146' into trunkEnrico Tassi
2016-06-16Ignore generated .ml file for ssrmatchingEnrico Tassi
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-16Fix another missing newlineJason Gross
2016-06-16Fix a printing typoJason Gross
Introduced by b21fefc0ec0aab2560d0b654f1a1f4203898388b
2016-06-16Fixing the checker.Pierre-Marie Pédrot
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.
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
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.
2016-06-15Fix test-suite for opened bug #4813.Pierre-Marie Pédrot
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
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.
2016-06-15ssrmatching: giving proper credits to the original author(s)Enrico Tassi
Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
2016-06-15Merge branch 'pr/146' into trunkEnrico Tassi
2016-06-15ssrmatching: simple test for Ltac APIEnrico Tassi
2016-06-15ssrmatching: ltac argument parsing made more robustEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 11:20:47 +0000