| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-16 | eauto: fix test-suite file | Matthieu Sozeau | |
| Now that typeclasses eauto uses the new eauto. | |||
| 2016-06-16 | bteauto: a Proofview.tactic for multiple goals | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | Typeclasses: allow shelved subgoals | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | Minor cleanup | Matthieu Sozeau | |
| 2016-06-16 | Typeclasses: refine the eauto tactic | Matthieu Sozeau | |
| - 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. | |||
| 2016-06-16 | Typeclasses: verbosity and Limit Intros options | Matthieu Sozeau | |
| 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! | |||
| 2016-06-16 | Proofview: extensions for backtracking eauto | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | typeclass resolution: add two compatibility options | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | setoid_rewrite: fix the Params resolution tactic | Matthieu Sozeau | |
| Add a substitution of a local variable by its body to ensure proper unification without having to make all local variables unfoldable. | |||
| 2016-06-16 | Fix incorrect caching of local hints w.r.t sections | Matthieu Sozeau | |
| 2016-06-16 | Compat with ocaml 4.01 | Matthieu Sozeau | |
| 2016-06-16 | Fix iterative deepening strategy failing too early | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | Implement limited proof search and iterative deepening. | Matthieu Sozeau | |
| Fix typo in proofview | |||
| 2016-06-16 | Typeclasses eauto based on new proof engine, | Matthieu Sozeau | |
| with full backtracking across multiple goals. | |||
| 2016-06-16 | Typeclasses: stdlib fixes for new search algorithm | Matthieu Sozeau | |
| 2016-06-16 | Refine 9cc95f5, unification of Let-In's, bug #3929 | Matthieu Sozeau | |
| 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. | |||
| 2016-06-16 | Small factorization in the typing flags of the kernel. | Pierre-Marie Pédrot | |
| 2016-06-16 | Factorizing the uses of Declareops.safe_flags. | Pierre-Marie Pédrot | |
| This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase. | |||
| 2016-06-16 | Adding a default safe set of kernel typing flags to Declareops. | Pierre-Marie Pédrot | |
| 2016-06-16 | Fixing a mispelling coma -> comma. | Hugo Herbelin | |
| 2016-06-16 | Typo in comment. | Hugo Herbelin | |
| 2016-06-16 | Fixing space in an error message. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of Register retroknowledge. | Hugo Herbelin | |
| 2016-06-16 | Fixing Add Parametric Relation by adding printer for binders. | Hugo Herbelin | |
| 2016-06-16 | Adding printers for ring and field commands. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of Function. | Hugo Herbelin | |
| 2016-06-16 | Isolating and exporting a function for printing body of a recursive definition. | Hugo Herbelin | |
| 2016-06-16 | Simplification in ppvernac.ml. | Hugo Herbelin | |
| 2016-06-16 | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr. | Hugo Herbelin | |
| No other changes (long only because of a change of indentation). | |||
| 2016-06-16 | Fixing extra space in printing bullets. | Hugo Herbelin | |
| 2016-06-16 | Fixing space in printing <+ and <: + fixing missing Inline keyword. | Hugo Herbelin | |
| Fixing : in Declare Module. | |||
| 2016-06-16 | Fixing printing of Instance. | Hugo Herbelin | |
| 2016-06-16 | Fixing extra space in printing abbreviations (SyntaxDefinition). | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of Polymorphic/Monomorphic. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of Arguments. | Hugo Herbelin | |
| 2016-06-16 | Printing notations as parsed. | Hugo Herbelin | |
| 2016-06-16 | So as to beautify to work, do not use notations in Inductive types | Hugo Herbelin | |
| with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance. | |||
| 2016-06-16 | Fixing missing substitution / printing cases of TacSelect. | Pierre-Marie Pédrot | |
| 2016-06-16 | Fixing parsing of constr argument of ltac functions at level 8 in the | Hugo Herbelin | |
| presence of entries starting with a non-terminal such as "b ^2". | |||
| 2016-06-16 | Fixing printing of keeping hyp on the fly. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of inversion as. | Hugo Herbelin | |
| 2016-06-16 | Fixing extra space in printing destruct/induction as. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of induction/destruct as. | Hugo Herbelin | |
| 2016-06-16 | Fixing printing of pat%constr. | Hugo Herbelin | |
| 2016-06-16 | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin | |
| 2016-06-16 | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin | |
| implicit is found whether one writes (sig P) or {x|P x}. | |||
| 2016-06-16 | Being defensive in printing implicit arguments also with manual | Hugo Herbelin | |
| implicit arguments when in beautification mode. | |||
| 2016-06-16 | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin | |
| simpler re-printing of assert. Also fixing the precedence for printing "by" clause. | |||
| 2016-06-16 | Changing rule for "*" in Operator_Properties so that, iterated, it | Hugo Herbelin | |
| does not print to ** which is a keyword. | |||
| 2016-06-16 | Protect the beautifier from change in the lexer state (typically by | Hugo Herbelin | |
| calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module"). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |