aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.mli
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
|
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
|
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
* | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Rework search_strategy option handlingGravatar Matthieu Sozeau2016-11-03
| |
| * Internal API change to typeclasses eauto.Gravatar Théo Zimmermann2016-11-03
| | | | | | | | | | | | | | This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking.
| * Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| |
| * Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
|/
* Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
|
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
| | | | Fix test-suite files
* 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: 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.
* 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.
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
|
* Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
|
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
| | | | | | being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine.
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Class_tactics between code and CAMLP4/5 declarations.Gravatar ppedrot2013-10-04
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 05:52:41 +0000