aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Allow camlp5 to have version numbers like "6.09-exp"Gravatar jbapple2014-10-28
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Removing dead code from Evd.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.diff function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the last Evd.diff from Hints.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.merge function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* Fixing clash in test destruct.v.Gravatar Hugo Herbelin2014-10-27
* Dead codeGravatar Hugo Herbelin2014-10-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:24:30 +0000