aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
2013-11-25Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
2013-11-24Better implementation of summary unfreezing.Pierre-Marie Pédrot
2013-11-24Adding fold_left / fold_right function to maps.Pierre-Marie Pédrot
2013-11-24Updating new ftp link to old archives.Hugo Herbelin
2013-11-24Hardening the reading function of vo files.Pierre-Marie Pédrot
2013-11-24Slightly more efficient zip function in Closure.Pierre-Marie Pédrot
2013-11-24Tweaking arity & allocation of some basic functions.Pierre-Marie Pédrot
2013-11-23Small allocation improvement in Closure.Pierre-Marie Pédrot
2013-11-23configure: typo in my last commitPierre Letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 06:17:39 +0000