| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-02 | Removing a redundancy in naming types (Ppconstr.precedence = tolerability). | Hugo Herbelin | |
| 2017-10-27 | Merge PR #6015: [general] Remove Econstr dependency from `intf` | Maxime Dénès | |
| 2017-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | |
| To this extent we factor out the relevant bits to a new file, ltac_pretype. | |||
| 2017-10-24 | An occurrence of set_id which behaves as the identity. | Hugo Herbelin | |
| 2017-10-10 | Parse [Proof using Type] without translating Type to an id. | Gaëtan Gilbert | |
| 2017-10-10 | [vernac] Remove "Proof using" hacks from parser. | Emilio Jesus Gallego Arias | |
| We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation. | |||
| 2017-10-03 | Implementing a generic mechanism for locating named objects from Coq side. | Pierre-Marie Pédrot | |
| 2017-10-03 | Moving the Ltac-specific part of the nametab to the Ltac plugin. | Pierre-Marie Pédrot | |
| For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit. | |||
| 2017-10-03 | Merge PR #1040: Efficient fresh name generation | Maxime Dénès | |
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | |
| We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | |
| The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | |||
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-25 | Merge PR #1057: Reporting locations in error messages about notation formats. | Maxime Dénès | |
| 2017-09-19 | Remove STM vernaculars. | Maxime Dénès | |
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau | |
| Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. | |||
| 2017-09-18 | Reporting locations in error messages about notation formats. | Hugo Herbelin | |
| 2017-09-15 | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | Maxime Dénès | |
| top of the linking chain. | |||
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-12 | Don't exclude a priori CLocalDef to be treated by ppconstr.ml. | Hugo Herbelin | |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-08-29 | [vernac] Store Infix Modifier in Vernac Notation. | Pierre-Marie Pédrot | |
| This removes a dependency from `G_vernac` to `Metasyntax`. | |||
| 2017-08-29 | Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵ | Maxime Dénès | |
| restructuration | |||
| 2017-08-29 | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | Maxime Dénès | |
| 2017-08-29 | A new step of restructuration of notations. | Hugo Herbelin | |
| This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20). | |||
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-01 | Printing goals does not evar-normalizes beforehand anymore. | Pierre-Marie Pédrot | |
| 2017-08-01 | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | |
| This was already the case, but the API was not exposing this. | |||
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-07-31 | Improve errors for cumulativity when monomorphic | Amin Timany | |
| We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. | |||
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Remove a few useless evar-normalizations in printing code. | Pierre-Marie Pédrot | |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
| 2017-07-20 | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | |
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | |
| We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | |||
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | |
| 2017-07-13 | The only abstraction-breaking function in Univ is now AUContext.instance. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for Global.body_of_constant and variants. | Pierre-Marie Pédrot | |
| We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. | |||
| 2017-07-11 | Moving the last bits of abtraction-breaking code out of the kernel. | Pierre-Marie Pédrot | |
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-06 | Merge PR #853: Clean 'with Definition' implementation. | Maxime Dénès | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-07-03 | Removing a few suspicious functions from the kernel. | Pierre-Marie Pédrot | |
| These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead. | |||
| 2017-06-25 | Moving "assert" (internally "Cut") to the new proof engine. | Hugo Herbelin | |
| It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>". | |||
| 2017-06-21 | [vernac] Remove stale bool parameter from `VernacStartTheoremProof` | Emilio Jesus Gallego Arias | |
| `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. | |||
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
| 2017-06-16 | Add printing of cumulativity in inductive types | Amin Timany | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |