aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
...
* | OptimizationGravatar Amin Timany2017-06-16
| | | | | | | | | | Only try using cumulativity in conversion/subtyping if the universe instances are non-empty
* | Use a smart map_constrGravatar Amin Timany2017-06-16
| |
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| |
* | Move univops from kernel to libraryGravatar Amin Timany2017-06-16
| |
* | Simplify Univ.mlGravatar Amin Timany2017-06-16
| |
* | Disable debug printingGravatar Amin Timany2017-06-16
| | | | | | | | Fix a mistake in record declaration
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| |
* | Fix bugsGravatar 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.
* | Fix cum/conv for inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | | Fall back to the equating levels in case inductive is not fully applied instead of failing.
* | Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
| |
* | Add subtyping inference for inductive typesGravatar Amin Timany2017-06-16
| |
* | Correct subtyping check for constructorsGravatar Amin Timany2017-06-16
| |
* | Fix typo in error messageGravatar Amin Timany2017-06-16
| |
* | Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
| |
* | 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.
* | New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
| |
* | Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
| |
* | Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613Gravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#448: Do not recompute twice the whnf of terms in conversion.Gravatar Maxime Dénès2017-06-14
|\ \ \
| | | * Remove some useless code in Term_typingGravatar Gaëtan Gilbert2017-06-13
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | The [let _typ = ...] comes from before universe polymorphism. In those times it was [let _typ, cst = ...] which produced something of use. The asserts come from 359e4ffe3 and before (2006 and before). In those times [Typeops.infer] rebuilt the term being typed, but nowadays the assert seems of little use.
* | | Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \
* | | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| | | |
| | | * [kernel] Improve proof using message, fixes bugzilla #3613Gravatar Emilio Jesus Gallego Arias2017-06-07
| | | |
* | | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
| |_|/ |/| |
* | | Merge PR#728: A few typos.Gravatar Maxime Dénès2017-06-06
|\ \ \
| | * | Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
| * | | A few typos.Gravatar Hugo Herbelin2017-06-04
| |/ /
* / / Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
* | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.Gravatar Maxime Dénès2017-05-29
|\ \
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | | Merge PR#646: Revised behavior on ill-formed identifiersGravatar Maxime Dénès2017-05-23
|\ \ \
* \ \ \ Merge PR#518: Faster universe unificationGravatar Maxime Dénès2017-05-23
|\ \ \ \
| | * | | Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
| |/ / / |/| | | | | | | | | | | | | | | Namely: Replacing (currently deactivated) warning on illegal ident by an error in strict mode and nothing in soft mode.
* | | | Merge PR#572: Replacing costly merges in UGraph.Gravatar Maxime Dénès2017-05-11
|\ \ \ \
* \ \ \ \ Merge PR#602: Fix more warningsGravatar Maxime Dénès2017-05-03
|\ \ \ \ \
* \ \ \ \ \ Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \
| | * | | | | Remove dead code in native compiler.Gravatar Maxime Dénès2017-05-02
| |/ / / / / |/| | | | |
* | | | | | Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \
* | | | | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | | | | |
* | | | | | | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | | | | |
* | | | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | let-ins
| | * | | | | | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | | | | | | |
| | * | | | | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | | | | | | |
| | * | | | | | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | | | | | | |
| | * | | | | | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| |/ / / / / / |/| | | | | |
| | | | * | | Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-04-27
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes.
* | | | | | COMMENT: Pre_env.envGravatar Matej Kosik2017-04-20
| | | | | |
* | | | | | correcting a typo in a commentGravatar Matej Kosik2017-04-20
| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 00:53:33 +0000