| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | |
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | |
| Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. | |||
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot | |
| This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Rewrite 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 | Equality API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Refine API using EConstr. | 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 | Pretyping 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 | |
| 2016-10-21 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
| 2016-08-06 | Using a dedicated kind of substitutions in evar name generation. | Pierre-Marie Pédrot | |
| This saves a quadratic allocation by replacing arrays with maps. | |||
| 2016-08-05 | Using the extended contexts in pretyping. | Pierre-Marie Pédrot | |
| In addition to sharing, we also delay the computation of the environment in a by-need fashion. | |||
| 2016-08-04 | Use sets instead of lists for names to avoid in evar generation. | Pierre-Marie Pédrot | |
| 2016-08-04 | Simplifying code in evar generation. | Pierre-Marie Pédrot | |
| We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences. | |||
| 2016-08-04 | Exporting the renaming API for evar declaration. | Pierre-Marie Pédrot | |
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |