aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
2014-08-26Fix compilation error due to commented code in previous commit by Hugo.Matthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-25Add an is_cofix tacticJason Gross
2014-08-25Prerequisite to fix stm test-suite when not in -localPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Clean up a comment in plugins/romega/ReflOmegaCoreJason Gross
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-25Correct a spelling mistakeJason Gross
2014-08-25factored out require_modifiers + bug fix.Gregory Malecha
2014-08-25coqdep comments counter is in the stackPierre Boutillier
2014-08-25a comment about the new state.Gregory Malecha
2014-08-25Support for Timeout n and From ..Gregory Malecha
2014-08-25Make coqdep find Require commands prefixed by TimeGregory Malecha
2014-08-25Fixing previous commit.Pierre-Marie Pédrot
2014-08-25Fixing a bug introduced in the extension of 'apply in' + simplifying code.Hugo Herbelin
2014-08-24Removing a unused legacy parsing rule.Pierre-Marie Pédrot
2014-08-24Fixing bug #3404.Pierre-Marie Pédrot
2014-08-24Enabling drag & drop on the source view widgets.Pierre-Marie Pédrot
2014-08-23Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherPierre-Marie Pédrot
2014-08-23Fix test-suite file.Matthieu Sozeau
2014-08-23Fixing ml-dot & mli-dot targets.Pierre-Marie Pédrot
2014-08-23Fixing bug #3533.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 20:50:25 +0000