aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
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-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15fix dev/base_include (thanks Zimmi48)Pierre Letouzey
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-14Merge PR#749: Normalize deprecation notices of ./configureMaxime Dénès
2017-06-14Merge PR#622: Change the default flag value for Refine.refineMaxime Dénès
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime 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
2017-06-14[travis] fix Software Foundation (one added Require Extraction)Pierre Letouzey
2017-06-14[travis] fix CoLoR by inserting some Require Import FunIndPierre Letouzey
2017-06-14Temporary overlays for bignums.Maxime Dénès
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Merge PR#766: Fix ocamldebug for the APIMaxime Dénès
2017-06-13Revert "[travis] temporary UniMath overlay"Théo Zimmermann
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-13[travis] overlay for cornPierre Letouzey
2017-06-13[travis] extra test ci-bignums (+factorize other scripts)Pierre Letouzey
2017-06-13[travis] overlay + extra deps for math-classes (and formal-topology)Pierre Letouzey
2017-06-13Documenting the change of default flag value of Refine.refine.Pierre-Marie Pédrot
2017-06-13[travis] adapt CoLoR compilation to depend on the bignum packagePierre Letouzey
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12[travis overlay] Partially Revert 013c0232953f1f58Jason Gross
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-12add overlaysMatej Košík
2017-06-12Fix ocamldebug for the APIGaëtan Gilbert
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-11Normalize deprecation notices of ./configureThéo Zimmermann
Always output a warning on stderr when a deprecated option is used.
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-07add overlaysMatej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Overlay.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Maxime Dénès
a flag suspectingly renamed in a clearer way
2017-06-04Added support for a side effect on constants in reduction functions.Thomas Sibut-Pinote
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.
2017-06-02Add an overlay for coq-dpdgraph for 8.7Jason Gross
2017-06-02Add coq-dpdgraph CIJason Gross
2017-06-02[travis] [fiat] Test also fiat-core.Emilio Jesus Gallego Arias
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
2017-05-31Adding overlay for math-comp.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:52:12 +0000