aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-11-23Fixing bug #3165.Pierre-Marie Pédrot
2013-11-22Remove some occurrences of obsolete operatorsStephane Glondu
2013-11-22configure: improve last fixPierre Letouzey
2013-11-22Using hashes in Summary, like the previous commit did with Dyn.Pierre-Marie Pédrot
2013-11-22Using hashes instead of strings in dynamic tags. In case of collision, anPierre-Marie Pédrot
2013-11-21configure: CAML_LD_LIBRARY_PATH is enriched, not overwrittenPierre Letouzey
2013-11-21configure: fix some issues with last commitPierre Letouzey
2013-11-21Fix various \r issues with windowsJason Gross
2013-11-21Field_theory: nicer notations for constants 0 1 ...Pierre Letouzey
2013-11-21updated .mailmapPierre Letouzey
2013-11-21Add Acc_intro_generator on top of all wf function proof (much much faster exe...Julien Forest
2013-11-20Adding Acc_intro_generator in order to help computations of Function in parti...forest
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 18:17:20 +0000