aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2013-11-03configure stript allows make v4.00pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 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-02A try/with was catching every exception.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17034 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
2013-11-02Cleanup of comments in bootstrap/Monads.vaspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17031 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02The repeat tactic now honors failure levels in ltac.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17030 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Documentation for the backtracking features.aspiwack
This required some reorganisation of the documentation of existing tacticals. I hope the result is consistent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17029 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Tacticals.New.tclWITHHOLES: clean up.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17027 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix congruence: normalise hypotheses with respect to evars.aspiwack
Detected in CompCert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Add primitives in Goal.V82 to access the goal in nf_evar'd form.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02push_rel_context: do not rename section variables.aspiwack
Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17024 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine now does iota reduction in addition to beta.aspiwack
Restores more compatibility with the earlier implementation of refine. Needed in ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17023 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix compilation of pattern matching wrt variables: alias.aspiwack
Aliases (as clause) are a bit tricky. In Goal True, refine match 0 with | S n as p => _ | _ => I end Must produce the goal n:nat, p := S n : nat |- True However, in the deep branches: refine match 0 with | S (S n as p) => _ | _ => I end The alias is used to give a name to the variable of the first S : p:nat, n:nat |- True Before this patch, the goal would be p:nat, n:nat, p:=p : nat |- True Alias was used both to name the variable of the first S and to alias it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17022 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Restore Zsqrt compat now that refine works fine with match.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17021 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
Compilation of pattern-matching used to systematically introduce a dummy alias x:=x in the typing environment for each variable x in the patterns (except for purely variable patterns which correctly alias the term being matched). This interfered badly with the new refine implementation. To correct this I changed the "all variables" case of pattern-matching compilation to check whether the term currently being matched is a term introduced by the user or a subterm which is necessarily a variable. In the latter case, no alias is introduced. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17020 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine: Tactics.New.refine does beta-reduction.aspiwack
Previously I had wrapped Tactics.New.refine with extra beta-reduction in extratactics.ml4, that is, only for Ltac. Ocaml plugins saw the version without reduction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17019 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactic give_up.aspiwack
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A tactic shelve_unifiable.aspiwack
Puts on the shelf every goals under focus on which other goals under focus depend. Useful when we want to solve these goals by unification (as in a first order proof search procedure, for instance). Also meant to be able to recover approximately the semantics of the old refine with the new implementation (use refine t; shelve_unifiable). TODO: bug dans l'example de shelve_unifiable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Made multiple-goal tactic work after all: .aspiwack
Internalization was done relative to a goal. It doesn't make sense in the case of all:. When we make a tactic with all: the environment for internalization is taken to be the global environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17016 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Make multiple-goal tactics possible after a tclTHEN.aspiwack
Tacinterp used to interprete every tactics inside a goal, making multiple-goal tactics act on a single goal anyway. Uses a simple heuristic to decide when a goal is not needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17015 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ↵aspiwack
at the wrong time. The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t)) had the correct semantics! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a shelve tactic.aspiwack
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monad.v: implements the writer monad in continuation passing style.aspiwack
Benefits: fewer pair constructed/destructed especially in split. Potential costs: plus and zero now have closures with 11 arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17012 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monad.v: implements the environment monad in continuation passing ↵aspiwack
style. Benefits: the underlying monads are not referenced in the "current" primitive. Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17011 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Factors the lifting of environment and writer monads in bootstrap/Monad.vaspiwack
Takes a few extra lines but is probably more robust to future changes. Doesn't change the extracted code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17010 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds an experimental exactly_once tactical.aspiwack
exactly_once t, will have a success if t has exactly once success. There are a few caveats: - The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics) - The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17009 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Normalise goals with respect to evars in the new tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17008 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Refine does beta-reductions.aspiwack
To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17006 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A dedicated view type for Proofview_gen.split.aspiwack
It doesn't seem to affect performances. But the generated code is slightly cleaner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17005 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactical once.aspiwack
[once t] does just as [t] but has exactly one success it [t] has at least one success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17004 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Corrects the semantics of the "+" tactical.aspiwack
- Treats goals independently - Honors failure levels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17003 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
As a result the use of the glist-style interface for manipulating goals has almost been removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02More Proofview.Goal.enter.aspiwack
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:56:20 +0000