aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-25Factoring: is_section_variable.Arnaud Spiwack
In 0c7a77, I inadvertantly re-defined an is_section_variable function.
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-25Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
Revealed by message on coq-club on 24/11/2013.
2013-11-24Better implementation of summary unfreezing.Pierre-Marie Pédrot
2013-11-24Adding fold_left / fold_right function to maps.Pierre-Marie Pédrot
2013-11-24Updating new ftp link to old archives.Hugo Herbelin
2013-11-24Hardening the reading function of vo files.Pierre-Marie Pédrot
2013-11-24Slightly more efficient zip function in Closure.Pierre-Marie Pédrot
2013-11-24Tweaking arity & allocation of some basic functions.Pierre-Marie Pédrot
2013-11-23Small allocation improvement in Closure.Pierre-Marie Pédrot
2013-11-23configure: typo in my last commitPierre Letouzey
2013-11-23Fixing bug #3165.Pierre-Marie Pédrot
2013-11-22Remove some occurrences of obsolete operatorsStephane Glondu
2013-11-22configure: improve last fixPierre Letouzey
Let's avoid the "if a=$(cmd ...)" since: - unless being a shell expert, it's not obvious it's testing the exit code of cmd. - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the exit code of cmd. Instead, we test the emptiness of the variable content afterwards
2013-11-22Using hashes in Summary, like the previous commit did with Dyn.Pierre-Marie Pédrot
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-21configure: CAML_LD_LIBRARY_PATH is enriched, not overwrittenPierre Letouzey
Keeping the earlier content of this variable is crucial for opam (at least). Thanks to François Bobot and Thomas Refis for this one...
2013-11-21configure: fix some issues with last commitPierre Letouzey
- after piping with | tr -d, an exit code was lost - suspicious use of " " inside a larger " ", we use ' ' now instead
2013-11-21Fix various \r issues with windowsJason Gross
Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153.
2013-11-21Field_theory: nicer notations for constants 0 1 ...Pierre Letouzey
2013-11-21updated .mailmapPierre Letouzey
2013-11-21Add Acc_intro_generator on top of all wf function proof (much much faster ↵Julien Forest
execution)
2013-11-20Adding Acc_intro_generator in order to help computations of Function in ↵forest
particular
2013-11-19Optimization: in case of empty substitution, merging is trivial.Pierre-Marie Pédrot
2013-11-19update .mailmap with my email now that I've used it in a commitPierre Letouzey
2013-11-19A .mailmap file for a nice git-shorlog displayPierre Letouzey
In particular, this file allows to merge duplicated identities of a same person. See man git shortlog for more details.
2013-11-18A file listing old svn branches and tagsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17095 85f007b7-540e-0410-9357-904b9bb8a0f7
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-16Better implementation for stores.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17093 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-15bugfix micromega: solved an ambiguous symbol resolutionfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17092 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-15Revert "Fast lookup_named in environments, based on maps instead of lists."ppedrot
Contrarily to my machine results, it seems that it tore down the performance of Coq on benchmarks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 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-14Update comments in matching.mli.aspiwack
The comments were inaccurate after r16533. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 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-13Fast lookup_named in environments, based on maps instead of lists.ppedrot
This was quite a severe performance bottleneck. Ideally, this data structure should be put into contexts, but the relevant type is transparent... For now, we stick to this inelegant workaround. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17086 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-13Adding an unsafe mapping function to maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17085 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-13Synchronizing the printer of tactic notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17084 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-12Useless computation in Goal handle augmentation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17083 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-09Moving notation types into grammar rule.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17076 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Cleaning and documenting Egramcoq.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17075 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Partial applications in Goal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17074 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:55:37 +0000