aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-08-23Tactics.unify in the new monad.Pierre-Marie Pédrot
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-21Removing unused parts of the Goal.sensitive monad.Pierre-Marie Pédrot
2014-08-21Removing a Goal.sensitive in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-21Improve consistency of whitespace (beautifier).Xavier Clerc
2014-08-21Improve consistency of whitespace (beautifier).Xavier Clerc
2014-08-21Space after [identity] coercion keywords (beautifier).Xavier Clerc
2014-08-21Avoid redundant spaces (beautifier).Xavier Clerc
2014-08-21Do not drop the locality qualifier (beautifier).Xavier Clerc
2014-08-21Make beautify-archive usable on non-GNU systems.Xavier Clerc
2014-08-19Removing a use of Goal.refine.Pierre-Marie Pédrot
2014-08-19New primitive allowing to modify refine handles.Pierre-Marie Pédrot
2014-08-18Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Matthieu Sozeau
2014-08-18Fixing unification of subterms identified by patterns.Hugo Herbelin
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-18Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toHugo Herbelin
2014-08-18A few more comments in tactics.mli and hippatern.ml.Hugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Spotted a source of failure of the constr printer in debugger.Hugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-18Fix test-suite files.Matthieu Sozeau
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-18Fixing include of debugger.Pierre-Marie Pédrot
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-08-16Better printing of Ltac values.Pierre-Marie Pédrot
2014-08-16Fixing too restrictive detection of resolution of evars in "apply in"Hugo Herbelin
2014-08-15More self-contained code for tclWITHHOLES.Pierre-Marie Pédrot
2014-08-15Removing unused Refiner.tclWITHHOLES.Pierre-Marie Pédrot
2014-08-14Remove confusing behavior of unify_with_subterm that could fail withMatthieu Sozeau
2014-08-14Fix program using an the unsubstituted type of the original obligationMatthieu Sozeau
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-14Restore the error-handling behavior of [change], which was silently failingMatthieu Sozeau
2014-08-14Fix elimschemes accessing directly the universe context of inductives (fixes ...Matthieu Sozeau
2014-08-13Fix test-suite files according to new parsing rule for application of primitiveMatthieu Sozeau
2014-08-13Small optimization in Cooking: do not construct identity substitutions.Pierre-Marie Pédrot
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-12Upgrading output tests.Hugo Herbelin
2014-08-12Bug #3469: fixing unterminated comment.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 20:30:27 +0000