aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-31More "open" by default for trace debugging.Hugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-31Listing a few examples of destruct showing unsatisfactory behaviors.Hugo Herbelin
2014-10-31Avoid "destruct H" to apply on H itself when H is a section variable.Hugo Herbelin
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-31STM: new worker for queriesEnrico Tassi
2014-10-31STM: reorganize code and file namesEnrico Tassi
2014-10-31Show_script called only if in coqtop modeEnrico Tassi
2014-10-30Better error messages when unfreezing summary entriesEnrico Tassi
2014-10-30Fix backtracking issue in Defined (Close 3780)Enrico Tassi
2014-10-28Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsNickolai Zeldovich
2014-10-28Haskell extraction: put unsafeCoerce type declaration laterNickolai Zeldovich
2014-10-28Allow camlp5 to have version numbers like "6.09-exp"jbapple
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-27Removing dead code from Evd.Pierre-Marie Pédrot
2014-10-27Removing the Evd.diff function.Pierre-Marie Pédrot
2014-10-27Removing the last Evd.diff from Hints.Pierre-Marie Pédrot
2014-10-27Removing the Evd.merge function.Pierre-Marie Pédrot
2014-10-27Removing an Evd.merge in Newring.Pierre-Marie Pédrot
2014-10-27Fixes for PG (Close 3763, 3770)Enrico Tassi
2014-10-27Make sure that Logic/ExtensionalityFacts gets compiled.Guillaume Melquiond
2014-10-27Fix some typos.Guillaume Melquiond
2014-10-27Use the url package, since coqdoc generates \url commands.Guillaume Melquiond
2014-10-27Making destruct on idents with maximal implicit arguments working, byHugo Herbelin
2014-10-27Ensuring compatibility when an hypothesis used for destruct isHugo Herbelin
2014-10-27Fixing evars lost in interpretation of eliminator of destruct.Hugo Herbelin
2014-10-27Fixing clash in test destruct.v.Hugo Herbelin
2014-10-27Dead codeHugo Herbelin
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-26Preventing potential evar leak in Rewrite.Pierre-Marie Pédrot
2014-10-26Applying like-first selection for destruct in hypotheses.Hugo Herbelin
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-26Dead code + typo.Hugo Herbelin
2014-10-25Changed implementation of lib/heap.ml to use Braun treesJean-Christophe Filliatre
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-25VarInstance are also goals.Hugo Herbelin
2014-10-24Install index_urls.txt in a location where coqide might actually find it.Guillaume Melquiond
2014-10-24Fix generation of the index_urls.txt file.Guillaume Melquiond
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-24Remove an ununsed pattern and commented code in the kernel.Matthieu Sozeau
2014-10-24Apparently, the former refine was simplifying in hypotheses too.Hugo Herbelin
2014-10-24Documenting some incompatibilities in (non) Import of ML tactics,Hugo Herbelin
2014-10-24Fixing order of hypothesis in goal hypotheses compaction for coqtop.Hugo Herbelin
2014-10-24Addressing report #3279 (inconsistency of behavior of the -> and <-Hugo Herbelin
2014-10-24Fix retroknowledge for int31 division.Maxime Dénès
2014-10-24-help failing (fix 3762)Enrico Tassi
2014-10-24Fix typo in documentation of the [repeat] tactical.Arnaud Spiwack
2014-10-24No hash consing across calls to the native compiler.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 14:37:48 +0000