aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Moving notation types into grammar rule.ppedrot
2013-11-09Cleaning and documenting Egramcoq.ppedrot
2013-11-09Partial applications in Goal.ppedrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-08Reverting the old LIFO behaviour of the notation finding algorithm.ppedrot
2013-11-08Removing partial applications in Reductionops.ppedrot
2013-11-08Useless array manipulation in Rtrees.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:25:53 +0000