| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-02-14 | Moving evar-normalization functions to EConstr. | Pierre-Marie Pédrot | |
| This removes code duplication between Evarutil and EConstr. | |||
| 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 | Making Evd independent from Namegen. | Pierre-Marie Pédrot | |
| 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 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2016-10-24 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-21 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
| 2016-09-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-05 | Fast path in push_rel_context_to_named_context. | Pierre-Marie Pédrot | |
| Essentially, we do not reconstruct the named_context_val when the rel_context is empty. | |||
| 2016-09-02 | Fast path in whd_evar. | Pierre-Marie Pédrot | |
| Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined. | |||
| 2016-08-26 | Removing calls of "Context.Rel.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-26 | CLEANUP: minor readability improvements | Matej Kosik | |
| 2016-08-25 | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵ | Matej Kosik | |
| "Context.{Rel,Named}.fold_constr" | |||
| 2016-08-24 | CLEANUP: minor readability improvements | Matej Kosik | |
| mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called. | |||
| 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-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵ | Pierre Letouzey | |
| module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not allocate a closure in the main loop, and do so only when needed. | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not check for presence of a variable in a global definition when we know that this variable was not present in the section. | |||
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |