| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-03 | Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760). | Maxime Dénès | |
| 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 computation of the names contained in an environment. | Pierre-Marie Pédrot | |
| 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 | Properly display the "only" prefix for selectors (bug #5760). | Guillaume Melquiond | |
| This commit also fixes range selectors being incorrectly displayed. | |||
| 2017-09-19 | Don't lose names in UState.universe_context. | Gaëtan Gilbert | |
| We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | |||
| 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-15 | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵ | Maxime Dénès | |
| work better on them | |||
| 2017-09-12 | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | |
| 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-09-07 | Merge PR #931: Parametrize module body | Maxime Dénès | |
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | |
| 2017-08-29 | Separating the module_type and module_body types by using a type parameter. | Pierre-Marie Pédrot | |
| As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12). | |||
| 2017-08-29 | Properly handling parameters of primitive projections in cctac. | Pierre-Marie Pédrot | |
| 2017-08-29 | Merge PR #946: Functional pretyping interface | Maxime Dénès | |
| 2017-08-29 | Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵ | Maxime Dénès | |
| restructuration | |||
| 2017-08-29 | Merge PR #805: Functional tactics | 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-29 | Adapting code to renaming Option.fold_map -> Option.fold_left_map. | Hugo Herbelin | |
| 2017-08-29 | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin | |
| (from module List). | |||
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #942: solving b1859 | Maxime Dénès | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-01 | Move type_uconstr to Tacinterp. | Maxime Dénès | |
| 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 #909: Extraction: reduce primitive projections in types (fix bug 4709) | Maxime Dénès | |
| 2017-08-01 | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND. | Maxime Dénès | |
| 2017-08-01 | Merge PR #806: closing bug 5315 | Maxime Dénès | |
| 2017-08-01 | adding a comment to explain the change | Julien Forest | |
| 2017-08-01 | solving b1859 | Julien Forest | |
| 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-31 | Correcting [build_discriminator] to make the test-suite pass | amblaf | |
| 2017-07-29 | closing bug 5315 | Julien Forest | |
| 2017-07-28 | Merge PR #889: Removing template polymorphism for definitions. | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Extraction: reduce primitive projections in types (fix bug 4709) | Pierre Letouzey | |
| 2017-07-26 | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵ | Maxime Dénès | |
| 4844 and 4824) | |||
| 2017-07-26 | Removing default evar-normalization for ARGUMENT EXTEND. | Pierre-Marie Pédrot | |
| This fixes bug 5650: evar (x : Prop) should not be slow. | |||
| 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-26 | Merge PR #905: [api] Remove type equalities from API. | Maxime Dénès | |
| 2017-07-26 | Merge PR #857: Extraction: various fixes related with bug 4720 | Maxime Dénès | |
| 2017-07-26 | Merge PR #859: Extraction TestCompile | Maxime Dénès | |
| 2017-07-25 | [api] Remove type equalities from API. | Emilio Jesus Gallego Arias | |
| This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli` | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |