aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-10-23Fixing order of declarations in the function which compacts variablesHugo Herbelin
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-23Taking into account factorization of consecutive names of same typesHugo Herbelin
2014-10-23fix parsing of ---- +++++ ***** in CoqIDEEnrico Tassi
2014-10-23Monad: change the error managing of two-list combinators.Arnaud Spiwack
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-23Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Arnaud Spiwack
2014-10-22Bugfix 3604 : more robust Unix.lockfFrédéric Besson
2014-10-22Fixing typo in output test Notations.Hugo Herbelin
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
2014-10-22Removing an unused variant of Context.fold_named_context_reverse.Hugo Herbelin
2014-10-22CoqIDE: fix parsing of multicharacter bulletsEnrico Tassi
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Make rint_location_in_file resilient to Cd (close 3630)Enrico Tassi
2014-10-22Fix the way lexeme start is computed (Close 3737)Enrico Tassi
2014-10-22Goal printing made uniform: always done in STM (close 3585)Enrico Tassi
2014-10-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-10-22Fix test-suite for #2729.Maxime Dénès
2014-10-22Fix missing lift in VM and native compiler (second part of #2729).Maxime Dénès
2014-10-22Refine tactic: simplify the conclusion only at the end of the tactic.Arnaud Spiwack
2014-10-22Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Arnaud Spiwack
2014-10-22Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Arnaud Spiwack
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-22CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...Arnaud Spiwack
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-22Fixing what really looks like a bug in the initial implementation ofHugo Herbelin
2014-10-22Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Hugo Herbelin
2014-10-22Fixing typo absorption (bug #3751).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 01:34:20 +0000