| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | Proofview.Goal primitive now return EConstrs. |  Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Eqdecide API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Class_tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Eauto API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Auto API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Leminv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Inv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Contradiction API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Equality API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Elim API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Hipattern API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Tacticals API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Clenv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Refine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Cleaning up opening of the EConstr module in pretyping folder. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| * | | | | Unification API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Cases API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Typeclasses API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Tacred API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Constr_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Patternops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Typing API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Evarsolve API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Find_subterm API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Retyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Reductionops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| * | | | | Termops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| | | | | | ||||
| | * | | | Proofview: tclINDEPENDENTL |  Enrico Tassi | 2017-02-10 | |
| | | | | | ||||
| | * | | | Fixing injection in the presence of let-in in constructors. |  Hugo Herbelin | 2016-12-22 | |
| | | | | | | | | | | | | | | | | | This also fixes decide equality, discriminate, ... (see e.g. #5279). | |||
| | * | | | Merge remote-tracking branch 'github/pr/172' into trunk |  Maxime Dénès | 2016-12-19 | |
| | |\ \ \ | | | | | | | | | | | | | | | | Was PR#172: alternate path separators in typeclass debug output. | |||
| | * \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 | |
| | |\ \ \ \ | | | |/ / | | |/| | | ||||
| | | * | | | Merge remote-tracking branch 'github/pr/381' into v8.6 | Maxime Dénès | 2016-12-02 | |
| | | |\ \ \ | | | | | | | | | | | | | | | | | | | Was PR#381: V8.6+fix typeclasses eauto shelving | |||
| | | | * | | | Fix shelving order in typeclasses eauto. |  Théo Zimmermann | 2016-11-30 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved. | |||
| | | | * | | | Fix typeclasses eauto shelving. | Théo Zimmermann | 2016-11-30 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| | | * | | | | Fix bug #5232: proper globalization of hints paths |  Matthieu Sozeau | 2016-11-30 | |
| | | |/ / / | ||||
| | * | | | | Tests for info/debug auto/eauto. | Hugo Herbelin | 2016-11-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is while waiting for a deeper uniformization of auto, eauto, and typeclasses eauto. Incidentally includes a little fix in harmonizing auto/eauto printing. | |||
| | * | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 | |
| |/| | | | | |/ / / | ||||
| | * | | | Minor debug printing bug, | Matthieu Sozeau | 2016-11-16 | |
| | | | | | | | | | | | | | | | | | Hit by OCaml's "if then else" with no "end" once more | |||
| | * | | | Revert more of a477dc for good measure | Matthieu Sozeau | 2016-11-16 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| | * | | | Revert part of a477dc, disallow_shelved | Matthieu Sozeau | 2016-11-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 | |||
| | * | | | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | 2016-11-07 | |
| | |\ \ \ | | | | | | | | | | | | | | | | Was PR#339: Documenting type class options, typeclasses eauto | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |