aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2013-11-18A file listing old svn branches and tagsletouzey
2013-11-16Slightly faster version of merging substitutions in TacticMatching.ppedrot
2013-11-16Better implementation for stores.ppedrot
2013-11-15bugfix micromega: solved an ambiguous symbol resolutionfbesson
2013-11-15Revert "Fast lookup_named in environments, based on maps instead of lists."ppedrot
2013-11-14Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...aspiwack
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
2013-11-14Update comments in matching.mli.aspiwack
2013-11-14Remove some dead code in tacinterp.aspiwack
2013-11-13Fast lookup_named in environments, based on maps instead of lists.ppedrot
2013-11-13Adding an unsafe mapping function to maps.ppedrot
2013-11-13Synchronizing the printer of tactic notations.ppedrot
2013-11-12Useless computation in Goal handle augmentation.ppedrot
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 07:29:16 +0000