aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Removing a unused legacy parsing rule.Gravatar Pierre-Marie Pédrot2014-08-24
* Fixing bug #3404.Gravatar Pierre-Marie Pédrot2014-08-24
* Enabling drag & drop on the source view widgets.Gravatar Pierre-Marie Pédrot2014-08-24
* Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherGravatar Pierre-Marie Pédrot2014-08-23
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-23
* Fixing ml-dot & mli-dot targets.Gravatar Pierre-Marie Pédrot2014-08-23
* Fixing bug #3533.Gravatar Pierre-Marie Pédrot2014-08-23
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a Goal.sensitive in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-18 22:06:50 +0000