aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2013-12-22Do not pass unification flags around in Rewrite.Pierre-Marie Pédrot
2013-12-22Slight code cleaning ensuring more static invariants in Rewrite.Pierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
internalization time.
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-19Using interp_genarg in tactic notations where possible, instead of an ad-hocPierre-Marie Pédrot
interpreter.
2013-12-19Bad use of Obj.magic in interpretation of TacAlias arguments.Pierre Boutillier
It triggered nonsensical behaviour of list-using tactic notation. Hopefully or not, nobody uses such notations out of the test-suite...
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values.
2013-12-16Get rid of messages "emitting ..." when compiling .v filesPierre Letouzey
If these messages are still relevent to somebody, feel free to restore them in -debug or any non-default mode of your choice.
2013-12-16Dedicated inductive for return values of rewrite strategies.Pierre-Marie Pédrot
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-09Stylistic change.Arnaud Spiwack
I doubt [catching_error] is performance critical in any way. But it looked silly to allocate a block to [(inner_trace,e)] when [e] was known in advance (and was already named [e]).
2013-12-04Vernac classification: allow for commands which start proofs but must be ↵Arnaud Spiwack
synchrone. The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
2013-12-02Porting type interpretation in Tacinterp to the new tactics.Pierre-Marie Pédrot
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-12-01Ensuring the right parsing of glob arguments, used by refinePierre-Marie Pédrot
and instantiate. Each of these tactics uses it at a different parsing level, thus actually triggering a parsing error after merging them. This fix implies some code duplication, which is a pity. The separation between genargs and parsing entries should be made one day.
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
2013-11-27Fixing abstract tactic by using a dummy name out of a declared proof.Pierre-Marie Pédrot
2013-11-27Adding the necessary hooks to handle tactics in terms.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
parsing is plugged.
2013-11-26Do not use ugly Dyn features in the Quote plugin. Use instead thePierre-Marie Pédrot
provided tactic environment to handle open terms.
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
Since the new proof engine, Hiddentac has been essentially trivial. Here is what happened to the functions defined there - Aliases, or tactics that were trivial to inline were systematically inlined - Tactics used only in tacinterp have been moved to tacinterp - Other tactics have been moved to a new module Tactics.Simple.
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics. I've changed some of them to explicitely take an environment and an evar_map instead.
2013-11-22Remove some occurrences of obsolete operatorsStephane Glondu
2013-11-22Using hashes instead of strings in dynamic tags. In case of collision, anPierre-Marie Pédrot
anomaly is raised. As there are very few tags defined in Coq code, this is very unlikely to appear, and can be fixed by tweaking the name of the dynamic argument. This should be more efficient, as we did compare equal strings each time.
2013-11-19Optimization: in case of empty substitution, merging is trivial.Pierre-Marie Pédrot
2013-11-16Slightly faster version of merging substitutions in TacticMatching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Changes the semantics of Ltac's non-lazy pattern matching in presence of ↵aspiwack
multiple successes. The semantics was a bit strange: an immediate failure of a branch would cause the pattern matching to backtrack, and failure after the match could cause the selected tactic to backtrack. However, the pattern matching process won't backtrack after it has selected a tactic with at least one success. To avoid changing the semantics of pattern matching with single-success tactics, I made it so that it is impossible to backtrack into a pattern matching once done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17090 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
The implementation was partly based on IStream and partly on a control flow with exception. The latter does not mix well with the monadic tactics. I've moved the algorithmic part of pattern-matching to a new file (tactics/tacticMatching.ml), in order to de-entangle the pattern-matching procedure from the interpretation. This shaves off 300 lines of code from Tacinterp, which is still over 2000 lines of code. It is a first step towards refactoring tacinterp. To be fair, part of what disapeared are lines which sent messages to the debugger. I was not too concerned with them because I understand people found the debugger much too fine-grain on Ltac's pattern matching. But conversely, there may be too few debugging hooks now. This is worth looking into. In TacticMatching itself, I used a monadic style to express the pattern-matching procedure concisely. I implemented the monad in a fairly brute-force way, using the existing primitive of IStream. It may be worth experimenting with specialized primitive. I am less worried about the monadic style than about the number of allocation of list cells that the primitives entail. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17089 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-14Remove some dead code in tacinterp.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17087 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was ↵aspiwack
solved. This made "autorewrite using tac" fail. Spotted in CoLoR and Demos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility. Spotted in Fermat4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not ↵aspiwack
caught by ltac tacticals. The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad). Spotted in ProjectiveGeometry and Goedel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix change: nf_evar prior to tactic interpretation.aspiwack
Noticed in PTSATR. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17056 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fixing CAMLP4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17039 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix set: nf_evar prior to tactic interpretation.aspiwack
Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17038 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Plug back infoH.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17037 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Plugs back external tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17036 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix the log of debug auto.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17035 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Update comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-16 12:13:40 +0000