aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Space after [identity] coercion keywords (beautifier).Gravatar Xavier Clerc2014-08-21
* Avoid redundant spaces (beautifier).Gravatar Xavier Clerc2014-08-21
* Do not drop the locality qualifier (beautifier).Gravatar Xavier Clerc2014-08-21
* Make beautify-archive usable on non-GNU systems.Gravatar Xavier Clerc2014-08-21
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
* Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Gravatar Matthieu Sozeau2014-08-18
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
* A few more comments in tactics.mli and hippatern.ml.Gravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Spotted a source of failure of the constr printer in debugger.Gravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fix test-suite files.Gravatar Matthieu Sozeau2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fixing include of debugger.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
* Better printing of Ltac values.Gravatar Pierre-Marie Pédrot2014-08-16
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Remove confusing behavior of unify_with_subterm that could fail withGravatar Matthieu Sozeau2014-08-14
* Fix program using an the unsubstituted type of the original obligationGravatar Matthieu Sozeau2014-08-14
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Restore the error-handling behavior of [change], which was silently failingGravatar Matthieu Sozeau2014-08-14
* Fix elimschemes accessing directly the universe context of inductives (fixes ...Gravatar Matthieu Sozeau2014-08-14
* Fix test-suite files according to new parsing rule for application of primitiveGravatar Matthieu Sozeau2014-08-13
* Small optimization in Cooking: do not construct identity substitutions.Gravatar Pierre-Marie Pédrot2014-08-13
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
* Bug #3469: fixing unterminated comment.Gravatar Hugo Herbelin2014-08-12
* In bug #2406, renouncing to test failure of parsing error.Gravatar Hugo Herbelin2014-08-12
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
* Fixing parsing of bullets after a "...".Gravatar Hugo Herbelin2014-08-12
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Allow pattern matching on the applied form of projections with primitiveGravatar Matthieu Sozeau2014-08-09
* Do early occur-check in unification to allow eta to fire (fixes bug #3477)Gravatar Matthieu Sozeau2014-08-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:13:08 +0000