aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Collapse)Author
2016-05-11Making the grammar command extend API purely functional.Pierre-Marie Pédrot
Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function.
2016-05-11Moving the constr empty entry registering to the state-based API.Pierre-Marie Pédrot
2016-05-11Turning the grammar extend command API into a state-passing one.Pierre-Marie Pédrot
2016-05-11Moving the grammar summary to Pcoq.Pierre-Marie Pédrot
2016-05-10AlistNsep token now accepts an arbitrary separator.Pierre-Marie Pédrot
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Pass user symbol to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Removing the Value.of_* API for parameterized types.Pierre-Marie Pédrot
Although still working, it is now bad practice to use it, and it is not widely spread anyway.
2016-05-04Do not generate generic arguments for data which only requires toplevel values.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Simplifying the code of Tacinterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-02Generate parsing rules for ML tactics in the same order as before a7917a32.Pierre-Marie Pédrot
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.
2016-05-02Useless code in Tacentries.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
2016-04-27Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Hugo Herbelin
This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6.
2016-04-27Revert "Fixing Add Parametric Relation by adding printer for binders."Hugo Herbelin
This reverts commit 36fb3d3a53418a81675815e47b3810e11bc31e4c.
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
2016-04-27Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Hugo Herbelin
This reverts commit df1e24f64f68318221d08246098837368ee1b406.
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
2016-04-27Revert "Fixing space in an error message."Hugo Herbelin
This reverts commit e0fd6e50800bc5aec4eafddd315941d6f7bc6efc.
2016-04-27Revert "Typo in comment."Hugo Herbelin
This reverts commit 239f30c2070018db88e568acca6c9054f650ca38.
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Hugo Herbelin
EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
2016-04-27Typo in comment.Hugo Herbelin
2016-04-27Fixing space in an error message.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
need at matching time rather than eagerly at the beginning of the call to "match". To be done for other constructs too, e.g. "match term with ... endp".
2016-04-27Passing around the precedence to the generic printer so as to solveHugo Herbelin
the remaining issue with the fix to #3709. However, this does not solve the problem in mind which is that "intuition idtac; idtac" is printed with extra parentheses into "intuition (idtac; idtac)". If one change the level of printing of TacArg of Tacexp from latom to inherited, this breaks elsewhere, with "let x := (simpl) in idtac" printed "let x := simpl in idtac".
2016-04-27A fix to #3709: ensuring extra parentheses when a tactic entry has aHugo Herbelin
subentry at a higher tactic level than the entry itself. This is applicable to the parsing of expressions with infix or postfix operators such as ; or ||. Could be improved, e.g. so that no parenthesis are put when the expression is the rightmost one, as in: now (tac1;tac2) where parentheses are not needed but still printed with this patch, while the patch adds needed parentheses in (now tac1);tac2 This would hardly scale to more complex grammars. E.g., if a suffix expression can extend a leading expression as part of different grammar entries, as in let x := simpl in y ... I don't see in general how to anticipate the need for parentheses without restarting the parser to check the reversibility of the printing.
2016-04-27Fixing printing of Register retroknowledge.Hugo Herbelin
2016-04-27Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-04-27Fixing 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-04-27Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
VERNAC EXTEND.
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
variables" when matching over "{v : _ | _ & _}" which hides twice the binding "fun v" since it is "sig2 (fun v => _) (fun v => _)". Computing the bound variables statically at internalisation time rather than every time at interpretation time. This cannot hurt even if I don't know how to deal with the "notation" problem of a single bound variable actually hiding two: at the current time, the notation is printed only if the two variables are identical (see #4592), so, with this semantics the warning should not be printed, but we lost the information that we are coming from a notation; if #4592 were addressed, then one of the binding should be alpha-renamed if they differ, so collision should be solved by choosing the variable name which is not renamed, but the matching algorithm should then be aware of what the notation printing algorithm is doing... maybe not the most critical thing at the current time.
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-25Factorizing code in tactic notations.Pierre-Marie Pédrot
2016-04-25Documenting API.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-09 03:14:54 +0000