aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-16Add printing of cumulativity in inductive typesAmin Timany
2017-06-16Move univops from kernel to libraryAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Simplify Univ.mlAmin Timany
2017-06-16Fix a bugAmin Timany
Incorrect environment was used when checking subtyping information of inductive types.
2017-06-16Disable debug printingAmin Timany
Fix a mistake in record declaration
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
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.
2017-06-16Make unification use subtyping info of inductivesAmin Timany
2017-06-16Fix cum/conv for inductive typesAmin Timany
Fall back to the equating levels in case inductive is not fully applied instead of failing.
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-16Change the place of inference after sect dischargeAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
Also reinferred after sections discharge
2017-06-16Add subtyping inference for inductive typesAmin Timany
2017-06-16Correct subtyping check for constructorsAmin Timany
2017-06-16Fix typo in error messageAmin Timany
2017-06-16Check subtyping of inductive types in KernelAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin 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-16New datastructure for universes of inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-06-15Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Maxime Dénès
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateMaxime Dénès
2017-06-15fix dev/base_include (thanks Zimmi48)Pierre Letouzey
2017-06-15Makefile.build : restore (temporarily?) the anti-cmi-corruption hacksPierre Letouzey
Due to the recent conversion of many .mli-only files into .ml files (hugely debatable impact of the API introduction), parallel make may fail badly again (always the same race between ocamlc and ocamlopt for .cmi). Still working on a proper fix, but meanwhile let's reintroduce the old hacks against these corruptions.
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-15Move Fiat to allowed failures.Maxime Dénès
For now, Fiat still relies on 8.4 compatibility.
2017-06-15Remove bedrock from test suite.Maxime Dénès
Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq.
2017-06-15Remove dependency on -compat flag in coq_makefile test suite.Maxime Dénès
2017-06-14Merge PR#749: Normalize deprecation notices of ./configureMaxime Dénès
2017-06-14Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Maxime Dénès
2017-06-14Merge PR#758: [toplevel] Print error header on fatal batch error.Maxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#765: Remove obsolete Show commandsMaxime Dénès
2017-06-14Merge PR#739: completing a sentence in a commentMaxime Dénès
2017-06-14Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Maxime Dénès
2017-06-14Merge PR#448: Do not recompute twice the whnf of terms in conversion.Maxime Dénès
2017-06-14Merge PR#622: Change the default flag value for Refine.refineMaxime Dénès
2017-06-14Merge PR#703: New version of the selective-unfolding PRMaxime Dénès
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14[print] Allow Selective Printing of NotationsEmilio Jesus Gallego Arias
We add new API to the printer to allows toggling the printing of individual notations and scopes: ```ocaml val toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit ``` This API is meant to be used by ML plugins. [this commit includes some refactoring by EJGA]
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime Dénès
2017-06-14Merge PR#220: Less init pluginsMaxime Dénès
2017-06-14[travis] overlay for fiat-crypto (a Require Import FunInd)Pierre Letouzey
2017-06-14[travis] overlays for CompCert and VST (an extra Require Export FunInd)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 19:50:18 +0000