aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
Commit message (Collapse)AuthorAge
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
| | | | | | Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
| |\
| | * Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
| | | | | | | | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ \ | | | | | | | | | | | | | | | | Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
| * | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | |/ | |/| | | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
| | | | | | | | | | | | | | | | | | The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase.
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic".
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
* | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\ \
| * | Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
| | | | | | | | | | | | variables and definitions in sections is unsupported.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
| * | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| | |
* | | Changing "P is assumed" to "P is declared".Gravatar Hugo Herbelin2016-01-14
| | | | | | | | | | | | | | | | | | | | | | | | The term "assumed" refers more to the type of the object than to the name of the object. It is particularly misguiding when P:Prop since P is assumed would suggest that a proof of P is assumed, and not that the variable P itself is declared (see discussion with P. Castéran on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015).
* | | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
|/ /
* | Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* | Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
| | | | | | | | involving Futures.
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large.
* | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
| | | | | | | | structure.
* | Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
| | | | | | | | | | | | | | context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time.
* | Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
| | | | | | | | | | | | According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions.
* | Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
| | | | | | | | No universe can be set lower than Prop anymore (or Set).
| * Propagate `Guarded` flag from syntax to kernel.Gravatar Arnaud Spiwack2015-09-25
| | | | | | | | The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
* | Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
| | | | | | | | with Enrico.
| * Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
|/ | | | The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
| | | | Of course such proofs cannot be processed asynchronously
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
| | | | | | into monomorphic constants, which was still using the de Bruijn encoding Bug revealed by discharging of hidden internal monomorphic definition in otherwise polymorphic developments. Makes coqchk work on Hurkens again.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
| | | | | | Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
| | | | | | | inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
| | | | | Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof.
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
| | | | | | | | | | | | | | Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
| | | | | | | for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array.
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
| | | | | | | | | | | now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
| | | | | | | | | | | Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-21 05:33:43 +0000