aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Merge branch 'nzgcd' into trunkGravatar Matthieu Sozeau2016-06-16
|\
| * Remove unneded hints in NZGcdGravatar Matthieu Sozeau2016-06-16
|/
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* Tentative fix of test-suite file to avoid loopGravatar Matthieu Sozeau2016-06-16
* Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
* Fix resolve_one_typeclass to use the new engineGravatar Matthieu Sozeau2016-06-16
* Bind resolve_one_typeclass to 8.5 or 8.6 resolutionGravatar Matthieu Sozeau2016-06-16
* Fix wrong tabulation in CHANGESGravatar Matthieu Sozeau2016-06-16
* Put autoapply back, lost during rebaseGravatar Matthieu Sozeau2016-06-16
* Cleanup and refactoringGravatar Matthieu Sozeau2016-06-16
* Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* Example given at DeepSpec workshopGravatar Matthieu Sozeau2016-06-16
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* eauto: fix test-suite fileGravatar Matthieu Sozeau2016-06-16
* bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
* Typeclasses: allow shelved subgoalsGravatar Matthieu Sozeau2016-06-16
* Minor cleanupGravatar Matthieu Sozeau2016-06-16
* Typeclasses: refine the eauto tacticGravatar Matthieu Sozeau2016-06-16
* Typeclasses: verbosity and Limit Intros optionsGravatar Matthieu Sozeau2016-06-16
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
* typeclass resolution: add two compatibility optionsGravatar Matthieu Sozeau2016-06-16
* setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
* Fix incorrect caching of local hints w.r.t sectionsGravatar Matthieu Sozeau2016-06-16
* Compat with ocaml 4.01Gravatar Matthieu Sozeau2016-06-16
* Fix iterative deepening strategy failing too earlyGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
* Small factorization in the typing flags of the kernel.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| * Adding a default safe set of kernel typing flags to Declareops.Gravatar Pierre-Marie Pédrot2016-06-16
|/
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
* Typo in comment.Gravatar Hugo Herbelin2016-06-16
* Fixing space in an error message.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-06-16
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-06-16
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
* Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-06-16
* Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-06-16
* Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-06-16
* Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Arguments.Gravatar Hugo Herbelin2016-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:56:06 +0000