aboutsummaryrefslogtreecommitdiffhomepage
path: root/API
Commit message (Collapse)AuthorAge
* Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵Gravatar Maxime Dénès2017-08-18
|\ | | | | | | with OCaml.
* \ Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \
| | | * Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
| |_|/ |/| | | | | | | | | | | Indeed OCaml has a similar file and this conflicts, at least in debugger.
| | * Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
| |/ |/| | | | | This was already the case, but the API was not exposing this.
* | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \
| | * Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
* | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ | |_|/ |/| |
* | | Merge PR #889: Removing template polymorphism for definitions.Gravatar Maxime Dénès2017-07-28
|\ \ \
* \ \ \ Merge PR #888: Stronger kernel typesGravatar Maxime Dénès2017-07-28
|\ \ \ \
* \ \ \ \ Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\ \ \ \ \
| | | | * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |_|_|/ / |/| | | |
| | | | * Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Pierre Letouzey2017-07-26
| |_|_|/ |/| | |
| | | * Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ |/| | | | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
* | Merge PR #905: [api] Remove type equalities from API.Gravatar Maxime Dénès2017-07-26
|\ \
* \ \ Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \ \
| | * | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`
* | | [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations.
| * | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | Avoid Anomaly (or Assert False) when a module signature contains an applied functor followed by a "with Definition" or "with Module" Also fix the dependency computation in presence of a "with Definition" Concerning 4720, the code extracted out of this bug report was suboptimal in Coq 8.4 (it was compilable, but could have probably been tweaked into a real issue producing faulty code). But the example of 4720 (and some variants of it) was broken since 8.5, for the same reasons as 5177 and 5240. And the good news is that after these repairs, the example of bug 4720 is now extracted to correct code (the "with" is preserved).
* | Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \
* | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
* | | Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
* | | Getting rid of AUContext abstraction breakers in Recordops.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | |
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
* | | [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
| | | | | | | | | | | | | | | `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
* | | Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \ \
* \ \ \ Merge PR#803: Clean ssrGravatar Maxime Dénès2017-06-20
|\ \ \ \
* \ \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR#784: API additions for coq-dpdgraphGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \
| | | | * | | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
| | | * | | Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
| | * | | A short cleanupGravatar Amin Timany2017-06-16
| | | | |
| | * | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| | | | |
| | * | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| | | | |
| | * | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
| | * | | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
| |/ / / |/| | |
* | | | Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \
* \ \ \ \ Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateGravatar Maxime Dénès2017-06-15
|\ \ \ \ \
| | | | | * API: Hints.run_hint,Pfedit.current_proof_statementGravatar Jason Gross2017-06-15
| |_|_|_|/ |/| | | | | | | | | | | | | | Add them for fiat-parsers
* | | | | Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \
* | | | | | | | API: exports Mltop.module_is_known to both API.mli and grammar_API.mliGravatar Pierre Letouzey2017-06-14
| | | | | | | |
| | | | | | * | API additions for coq-dpdgraphGravatar Gaëtan Gilbert2017-06-14
| |_|_|_|_|/ / |/| | | | | |
| | | | | * | G_prim: the bigint entry keeps numbers in raw stringsGravatar Pierre Letouzey2017-06-14
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 09:55:13 +0000