aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* Preventing potential evar leak in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-26
* Applying like-first selection for destruct in hypotheses.Gravatar Hugo Herbelin2014-10-26
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
* Changed implementation of lib/heap.ml to use Braun treesGravatar Jean-Christophe Filliatre2014-10-25
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* VarInstance are also goals.Gravatar Hugo Herbelin2014-10-25
* Install index_urls.txt in a location where coqide might actually find it.Gravatar Guillaume Melquiond2014-10-24
* Fix generation of the index_urls.txt file.Gravatar Guillaume Melquiond2014-10-24
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* Apparently, the former refine was simplifying in hypotheses too.Gravatar Hugo Herbelin2014-10-24
* Documenting some incompatibilities in (non) Import of ML tactics,Gravatar Hugo Herbelin2014-10-24
* Fixing order of hypothesis in goal hypotheses compaction for coqtop.Gravatar Hugo Herbelin2014-10-24
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
* Fix retroknowledge for int31 division.Gravatar Maxime Dénès2014-10-24
* -help failing (fix 3762)Gravatar Enrico Tassi2014-10-24
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
* No hash consing across calls to the native compiler.Gravatar Maxime Dénès2014-10-24
* Fixing order of declarations in the function which compacts variablesGravatar Hugo Herbelin2014-10-23
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
* fix parsing of ---- +++++ ***** in CoqIDEGravatar Enrico Tassi2014-10-23
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
* Evd.future_goals: forgot to revert the list in two places.Gravatar Arnaud Spiwack2014-10-23
* Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Gravatar Arnaud Spiwack2014-10-23
* Bugfix 3604 : more robust Unix.lockfGravatar Frédéric Besson2014-10-22
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* Removing an unused variant of Context.fold_named_context_reverse.Gravatar Hugo Herbelin2014-10-22
* CoqIDE: fix parsing of multicharacter bulletsGravatar Enrico Tassi2014-10-22
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Make rint_location_in_file resilient to Cd (close 3630)Gravatar Enrico Tassi2014-10-22
* Fix the way lexeme start is computed (Close 3737)Gravatar Enrico Tassi2014-10-22
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
* Fix test-suite for #2729.Gravatar Maxime Dénès2014-10-22
* Fix missing lift in VM and native compiler (second part of #2729).Gravatar Maxime Dénès2014-10-22
* Refine tactic: simplify the conclusion only at the end of the tactic.Gravatar Arnaud Spiwack2014-10-22
* Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Gravatar Arnaud Spiwack2014-10-22
* Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Gravatar Arnaud Spiwack2014-10-22
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...Gravatar Arnaud Spiwack2014-10-22
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* Fixing what really looks like a bug in the initial implementation ofGravatar Hugo Herbelin2014-10-22
* Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Gravatar Hugo Herbelin2014-10-22
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
* Proofview: documentation and re-ordering.Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 14:57:39 +0000