aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-16Remove unneded hints in NZGcdMatthieu Sozeau
2016-06-16proof mode: print unification constraintsMatthieu Sozeau
2016-06-16Tentative fix of test-suite file to avoid loopMatthieu Sozeau
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-06-16Fix resolve_one_typeclass to use the new engineMatthieu Sozeau
2016-06-16Bind resolve_one_typeclass to 8.5 or 8.6 resolutionMatthieu Sozeau
2016-06-16Fix wrong tabulation in CHANGESMatthieu Sozeau
2016-06-16Put autoapply back, lost during rebaseMatthieu Sozeau
2016-06-16Cleanup and refactoringMatthieu Sozeau
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-16Example given at DeepSpec workshopMatthieu Sozeau
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16eauto: fix test-suite fileMatthieu Sozeau
2016-06-16bteauto: a Proofview.tactic for multiple goalsMatthieu Sozeau
2016-06-16Typeclasses: allow shelved subgoalsMatthieu Sozeau
2016-06-16Minor cleanupMatthieu Sozeau
2016-06-16Typeclasses: refine the eauto tacticMatthieu Sozeau
2016-06-16Typeclasses: verbosity and Limit Intros optionsMatthieu Sozeau
2016-06-16Proofview: extensions for backtracking eautoMatthieu Sozeau
2016-06-16typeclass resolution: add two compatibility optionsMatthieu Sozeau
2016-06-16setoid_rewrite: fix the Params resolution tacticMatthieu Sozeau
2016-06-16Fix incorrect caching of local hints w.r.t sectionsMatthieu Sozeau
2016-06-16Compat with ocaml 4.01Matthieu Sozeau
2016-06-16Fix iterative deepening strategy failing too earlyMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-06-16Refine 9cc95f5, unification of Let-In's, bug #3929Matthieu Sozeau
2016-06-16Small factorization in the typing flags of the kernel.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Adding a default safe set of kernel typing flags to Declareops.Pierre-Marie Pédrot
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Typo in comment.Hugo Herbelin
2016-06-16Fixing space in an error message.Hugo Herbelin
2016-06-16Fixing printing of Register retroknowledge.Hugo Herbelin
2016-06-16Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-06-16Adding printers for ring and field commands.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-06-16Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-06-16Simplification in ppvernac.ml.Hugo Herbelin
2016-06-16Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
2016-06-16Fixing extra space in printing bullets.Hugo Herbelin
2016-06-16Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
2016-06-16Fixing printing of Instance.Hugo Herbelin
2016-06-16Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-06-16Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-06-16Fixing printing of Arguments.Hugo Herbelin
2016-06-16Printing notations as parsed.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 03:24:10 +0000