aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-11-08Do not compute formatter UTF8 length at creation time.ppedrot
2013-11-07Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
2013-11-07Partial application hunt.ppedrot
2013-11-06Partial application in Globnames.ppedrot
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-11-06better IStream.concatppedrot
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
2013-11-05Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeppedrot
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
2013-11-04Nicer infered names in refine.aspiwack
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...aspiwack
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...aspiwack
2013-11-04Fix change: nf_evar prior to tactic interpretation.aspiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-04Using allocation-free version of Array higher-order function in criticalppedrot
2013-11-04Adding closure-preventing functions in CArray. These functions are allppedrot
2013-11-04Allocation friendly version of Util.iterate.ppedrot
2013-11-04Added an update function in CMap. It has the same signature as Map.add, butppedrot
2013-11-04Manual coding of Int.Map.find. We use unsafe features, but this functionppedrot
2013-11-04Evar module now uses default Int maps and sets.ppedrot
2013-11-03empty token in terminal is a user error not an anomaly (bug 3118)pboutill
2013-11-03test-suite fixuppboutill
2013-11-03Asks camlp5 binary in path its locationpboutill
2013-11-03Fixup bug 3145pboutill
2013-11-03configure stript allows make v4.00pboutill
2013-11-02Fixing CAMLP4 compilation.ppedrot
2013-11-02Fix set: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Plug back infoH.aspiwack
2013-11-02Plugs back external tactics.aspiwack
2013-11-02Fix the log of debug auto.aspiwack
2013-11-02A try/with was catching every exception.aspiwack
2013-11-02Update comments.aspiwack
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
2013-11-02Cleanup of comments in bootstrap/Monads.vaspiwack
2013-11-02The repeat tactic now honors failure levels in ltac.aspiwack
2013-11-02Documentation for the backtracking features.aspiwack
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Tacticals.New.tclWITHHOLES: clean up.aspiwack
2013-11-02Fix congruence: normalise hypotheses with respect to evars.aspiwack
2013-11-02Add primitives in Goal.V82 to access the goal in nf_evar'd form.aspiwack
2013-11-02push_rel_context: do not rename section variables.aspiwack
2013-11-02Refine now does iota reduction in addition to beta.aspiwack
2013-11-02Fix compilation of pattern matching wrt variables: alias.aspiwack
2013-11-02Restore Zsqrt compat now that refine works fine with match.aspiwack
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
2013-11-02Refine: Tactics.New.refine does beta-reduction.aspiwack
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02A tactic shelve_unifiable.aspiwack
2013-11-02Made multiple-goal tactic work after all: .aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 17:23:54 +0000