aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2013-11-08Reverting the old LIFO behaviour of the notation finding algorithm.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17072 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Removing partial applications in Reductionops.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17071 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Useless array manipulation in Rtrees.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17070 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Do not compute formatter UTF8 length at creation time.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17069 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-07Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
going through a Coq extraction phase. We use second order quantification through OCaml records, which allows for a very precise use of low-level application. This results in quite a remarkable speedup but there is still room for improvement. This code was written by translating straightforwardly the Coq generated code in a human-readable dialect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-07Partial application hunt.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06Partial application in Globnames.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17066 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06better IStream.concatppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17064 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17063 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeppedrot
the argument list is consumed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17062 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
PG sends "Set Silent" and it was messing up the DAG, making the detection of an immediate proof not working. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17061 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Nicer infered names in refine.aspiwack
When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 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-04Using allocation-free version of Array higher-order function in criticalppedrot
cases, which are precisely term manipulation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17054 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Adding closure-preventing functions in CArray. These functions are allppedrot
higher-order functions like map and iter, and they are modified so that they take one additional argument, thus saving a cloure allocation. Compare the following. Array.iter: ('a -> unit) -> 'a array -> unit Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not allocate a closure. For now only the most critical functions are recoded. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17053 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Allocation friendly version of Util.iterate.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17052 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Added an update function in CMap. It has the same signature as Map.add, butppedrot
expects the given key to be present, and thus is faster. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17051 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Manual coding of Int.Map.find. We use unsafe features, but this functionppedrot
is quite critical indeed, as it is one of the most used throughout Coq executions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17050 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Evar module now uses default Int maps and sets.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17049 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-03empty token in terminal is a user error not an anomaly (bug 3118)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17047 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-03test-suite fixuppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17046 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-03Asks camlp5 binary in path its locationpboutill
before looking in CAMLLIB/camlp5 folder Patch by Thomas Braibant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17045 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-03Fixup bug 3145pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17043 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:48:59 +0000