aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Patternops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Find_subterm API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2016-12-22Fixing injection in the presence of let-in in constructors.Hugo Herbelin
This also fixes decide equality, discriminate, ... (see e.g. #5279).
2016-12-19Merge remote-tracking branch 'github/pr/172' into trunkMaxime Dénès
Was PR#172: alternate path separators in typeclass debug output.
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
Was PR#381: V8.6+fix typeclasses eauto shelving
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved.
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl.
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-19Tests for info/debug auto/eauto.Hugo Herbelin
This is while waiting for a deeper uniformization of auto, eauto, and typeclasses eauto. Incidentally includes a little fix in harmonizing auto/eauto printing.
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-16Minor debug printing bug,Matthieu Sozeau
Hit by OCaml's "if then else" with no "end" once more
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly.
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
Was PR#339: Documenting type class options, typeclasses eauto
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-05More precise refine compatibilityMatthieu Sozeau
2016-11-04Fix #3441 Use pf_get_type_of to avoid blowupMatthieu Sozeau
... in pose proof of large proof terms
2016-11-04Fix refine in compatibility modeMatthieu Sozeau
2016-11-04Merge remote-tracking branch 'github/pr/335' into v8.6Maxime Dénès
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
Was PR#336: Remove v62
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Internal API change to typeclasses eauto.Théo Zimmermann
This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking.
2016-11-03Do not shelve non-class subgoals but fail, it shouldMatthieu Sozeau
be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc.
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
2016-11-03Fix [typeclasses eauto with] and nopattern hintsMatthieu Sozeau
This was the source of a bug in #5115#c7.
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Handle Unique Solutions flag.Matthieu Sozeau
2016-11-03TCS: error handling and debug printing in resolutionMatthieu Sozeau
2016-11-03Fix bugs in Filtered Unification and cleanup codeMatthieu Sozeau
2016-11-03Fix Typeclasses eauto := bfs.Matthieu Sozeau
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
Was PR#321: Handling of section variables in hints
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
Was PR#338: Remove warning now that info_auto is fixed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 05:40:40 +0000