| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-14 | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | |
| Now they are useless because all of the primitives are (should?) be evar-insensitive. | |||
| 2017-02-14 | Fix a mishandled exception in Omega. | Pierre-Marie Pédrot | |
| Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly. | |||
| 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 compatibility layers from Tacticals | Pierre-Marie Pédrot | |
| 2017-02-14 | Omega API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Micromega API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | |
| 2017-02-14 | Funind API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing compatibility layers related to printing. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Setoid_ring API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Cc API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Quote API using EConstr. | Pierre-Marie Pédrot | |
| 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 | |
| 2017-02-08 | Merge PR#393: Replace Typeops with Fast_typeops | Maxime Dénès | |
| 2017-02-07 | Revert "Extraction: avoid deprecated functions of module String" | Pierre Letouzey | |
| This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry... | |||
| 2017-02-07 | Extraction cosmetic: no whitespaces in printing empty modules | Pierre Letouzey | |
| 2017-02-07 | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore | Pierre Letouzey | |
| 2017-02-07 | Extraction: avoid deprecated functions of module String | Pierre Letouzey | |
| - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |