aboutsummaryrefslogtreecommitdiff
path: root/ltac/tacsubst.ml
AgeCommit message (Collapse)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
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.
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
2016-06-16Fixing missing substitution / printing cases of TacSelect.Pierre-Marie Pédrot
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-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.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-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-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot