aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-30Adding printing of ltac envs to debugger.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-30Better heuristic for name generation backward compatibility. We fallbackPierre-Marie Pédrot
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
2013-11-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2013-11-29Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notHugo Herbelin
2013-11-29Testsuite: flatten the 'bugs/opened' directory.xclerc
2013-11-28Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)xclerc
2013-11-27Getting rid of goal-dependency in declarative mode argument evaluation.Pierre-Marie Pédrot
2013-11-27Fixing abstract tactic by using a dummy name out of a declared proof.Pierre-Marie Pédrot
2013-11-27Actually adding the grammar entry to handle tactics in terms.Pierre-Marie Pédrot
2013-11-27Adding the necessary hooks to handle tactics in terms.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-27Old message Interp returns the state id so that one can BackTo itEnrico Tassi
2013-11-27New option --help-XML-protocol to document the XML procol used by -ideslaveEnrico Tassi
2013-11-27First stab at retrocompatible INTERP messageEnrico Tassi
2013-11-27Use my real email address in .mailmapEnrico Tassi
2013-11-27Reduction: every n iterations a slaves process checks for interruptionEnrico Tassi
2013-11-27STM: restart slave after every proofEnrico Tassi
2013-11-27CoqIDE: show error message for parsing errorsEnrico Tassi
2013-11-26Adding a generic Int.Map using persistent arrays.Pierre-Marie Pédrot
2013-11-26Do not use ugly Dyn features in the Quote plugin. Use instead thePierre-Marie Pédrot
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 15:18:19 +0000