aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Remove unneded hints in NZGcdGravatar Matthieu Sozeau2016-06-16
| | | | They were already commented out, Pierre confirms they're spurious.
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
| | | | along with goals, with nice formatting.
* Tentative fix of test-suite file to avoid loopGravatar Matthieu Sozeau2016-06-16
| | | | | Looping on jenkins only, couldn't reproduce locally. To be investigated further.
* 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
| | | | | | | Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
| | | | | As noticed by C. Cohen it was confusingly different from standard notation.
* Example given at DeepSpec workshopGravatar Matthieu Sozeau2016-06-16
|
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
| | | | Fix test-suite files
* eauto: fix test-suite fileGravatar Matthieu Sozeau2016-06-16
| | | | Now that typeclasses eauto uses the new eauto.
* bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
| | | | | | | Add an option to force backtracking at toplevel, which is used by default when calling typeclasses eauto on a set of goals. They might be depended on by other subgoals, so the tactic should be backtracking by default, a once can make it not backtrack.
* Typeclasses: allow shelved subgoalsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | Be more lenient, allowing non-class subgoals to remain after resolution, this seems necessary when launching resolution in goals containing evars. Also put a tclONCE when hints don't need to backtrack.
* Minor cleanupGravatar Matthieu Sozeau2016-06-16
|
* Typeclasses: refine the eauto tacticGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | - Treat shelved dependent subgoals that might not be resolved after some proof search correctly by restarting their resolution as soon as possible (if they are typeclasses in only_classes mode). - Treat dependencies between goals better, avoiding backtracking more often when dependencies allow.
* Typeclasses: verbosity and Limit Intros optionsGravatar Matthieu Sozeau2016-06-16
| | | | | | | To deactivate the limitation of introductions (which was added to avoid eta expansions in proof terms). This can cause huge blowups due to dumb backtracking. The arrow introduction rule is reversible, so better do it eagerly!
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | unshelve_goals is used to correctly register dependent subgoals that have to be solved. Resolution may fail to do so using hints, so we have to put them back as goals in that case. The shelf is a good interface for doing that. unifiable can be used outside proofview to detect dependencies between goals. This might be better in another module.
* typeclass resolution: add two compatibility optionsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | Set Typeclasses Compatibility "8.5". uses the old resolution tactic (off by default, but useful for debugging incompatibilities) Set Typeclasses Unification Compatibility "8.5". uses the old clenv unification tactic in resolution even with the new proof engine (on by default for now). Also fix the 8.5-compatible unification with the new engine resolution function, by using with_shelf and unshelve.
* setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
| | | | | | Add a substitution of a local variable by its body to ensure proper unification without having to make all local variables unfoldable.
* 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
| | | | | | Report limit exceeded on _any_ branch so that we pursue search if it was reached at least once. Add example by N. Tabareau in test-suite.
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
| | | | Fix typo in proofview
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
| | | | with full backtracking across multiple goals.
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
|
* Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
| | | | | | | We unify types of let-ins in FO heuristic before their bodies, using cumulativity in either direction. This maintains the invariant that we are comparing terms in related types throughout unification. Also adapt test-suite file for bug #3929.
* 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
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
| * 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
| | | | No other changes (long only because of a change of indentation).
* 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 : in Declare Module.
* 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
|
* Printing notations as parsed.Gravatar Hugo Herbelin2016-06-16
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:53:40 +0000