| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | 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 | Rewrite API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Hints 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 | Tacmach 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 | |
| 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-14 | 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 | 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 | 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 | |
| 2016-10-31 | Moving unused code out of the kernel into Termops. | Pierre-Marie Pédrot | |
| Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there. | |||
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-28 | Merge remote-tracking branch 'github/pr/319' into v8.6 | Maxime Dénès | |
| Was PR#319: More error tagging, try to fix bug 5135 | |||
| 2016-10-25 | Merge commit 'a799600' into v8.6 | Maxime Dénès | |
| Was PR#334: Fix bug 5031 : should not be an anomaly | |||
| 2016-10-25 | That Function is unable to create a Fixpoint equation is a user problem, | Yves Bertot | |
| not an anomaly | |||
| 2016-10-24 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-24 | ssrmatching: fix interpretation of rpattern | Enrico Tassi | |
| 2016-10-19 | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript". | Matej Kosik | |
| The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting | |||
| 2016-10-18 | [pp] Use more convenient pp API in ssrmatching | Emilio Jesus Gallego Arias | |
| 2016-10-18 | [pp] Add tagging function to all low-level printing calls. | Emilio Jesus Gallego Arias | |
| The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases. | |||
| 2016-10-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-17 | Fix bug #5023: JSON extraction doesn't generate "for xxx". | Pierre-Marie Pédrot | |
| 2016-10-02 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-29 | Ncring_initial: avoid a notation overriding | Pierre Letouzey | |
| 2016-09-29 | Extraction: ignore some useless stuff about universes | Pierre Letouzey | |
| 2016-09-28 | Ring_theory: avoid overriding a few notations | Pierre Letouzey | |
| 2016-09-28 | Adding interface files to Nsatz ML files. | Pierre-Marie Pédrot | |
| 2016-09-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-26 | Fast russian peasant exponentiation in Nsatz. | Pierre-Marie Pédrot | |
| 2016-09-26 | Monomorphizing various uses of arrays in Nsatz. | Pierre-Marie Pédrot | |
| 2016-09-26 | Partial fix for bug #5085: nsatz_compute stack overflows. | Pierre-Marie Pédrot | |
| This fixes the stack overflow part of the bug, even if the tactic is still quite slow. The offending functions have been written in a tail-recursive way. | |||
| 2016-09-23 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |