aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2017-02-14Eqdecide API using EConstr.Pierre-Marie Pédrot
2017-02-14Class_tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Eauto API using EConstr.Pierre-Marie Pédrot
2017-02-14Auto API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Contradiction API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Elim API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 02:28:20 +0000