| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2017-06-16 | Fix bugs and add an option for cumulativity | Amin Timany | |
| 2017-06-16 | Using UInfoInd for universes in inductive types | Amin Timany | |
| It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. | |||
| 2017-06-15 | Merge PR#719: Constrexpr.Numeral without bigint | Maxime Dénès | |
| 2017-06-15 | Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state | Maxime Dénès | |
| 2017-06-14 | Merge PR#763: [proof] Deprecate redundant wrappers. | Maxime Dénès | |
| 2017-06-14 | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) | Pierre Letouzey | |
| This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml | |||
| 2017-06-12 | [proof] Move bullets to their own module. | Emilio Jesus Gallego Arias | |
| Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file. | |||
| 2017-06-12 | [lib] Remove obsolete state-management function add_frozen_state | Emilio Jesus Gallego Arias | |
| AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |