From 9a14a95f96c77ff3850d694637738358c164f4b5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 8 Jun 2017 11:17:22 +0200
Subject: Normalize deprecation notices of ./configure

Always output a warning on stderr when a deprecated option is used.
---
 dev/doc/setup.txt | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 1b016a4e26..0c6d3ee80d 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -12,7 +12,7 @@ How to compile Coq
 
 Getting build dependencies:
 
-  sudo apt-get install make opam git mercurial darcs
+  sudo apt-get install make opam git
   opam init --comp 4.02.3
   # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files.
   
@@ -41,7 +41,7 @@ Building coqtop:
   cd ~/git/coq
   git checkout trunk
   make distclean
-  ./configure -annotate -with-doc no -local -debug -usecamlp5
+  ./configure -annotate -local
   make clean
   make -j4 coqide printers
 
@@ -49,8 +49,6 @@ The "-annotate" option is essential when one wants to use Merlin.
 
 The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install
 
-The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary.
-
 Then check if
 - bin/coqtop
 - bin/coqide
@@ -60,7 +58,7 @@ behave as expected.
 A note about rlwrap
 -------------------
 
-Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try:
+Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try:
 
   cd ~/git/coq
   rlwrap bin/coqtop
-- 
cgit v1.2.3


From 649cc52200303abe4559d4c501c8aca06eed7591 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 12 Jun 2017 12:07:34 -0400
Subject: [travis overlay] Partially Revert 013c0232953f1f58

I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed---
 dev/ci/ci-basic-overlay.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7a9df93c45..03cf0a9d14 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,14 +97,14 @@
 ########################################################################
 # bedrock_src
 ########################################################################
-: ${bedrock_src_CI_BRANCH:=trunk__API}
-: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=master}
+: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # bedrock_facade
 ########################################################################
-: ${bedrock_facade_CI_BRANCH:=trunk__API}
-: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=master}
+: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # formal-topology
-- 
cgit v1.2.3


From 3cfb38cb0e5491d13a6ef5cda81dfec7f979cced Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 May 2017 17:28:23 +0200
Subject: Documenting the change of default flag value of Refine.refine.

---
 dev/doc/changes.txt | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index bcda4ff50a..8456195e6b 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -144,6 +144,9 @@ In Coqlib / reference location:
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
+- The Refine.refine function and its variants now have the unsafe flag turned
+  down by default.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
-- 
cgit v1.2.3


From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 dev/doc/changes.txt     | 4 ++--
 dev/doc/proof-engine.md | 7 +++----
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8456195e6b..63c064d843 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -144,8 +144,8 @@ In Coqlib / reference location:
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
-- The Refine.refine function and its variants now have the unsafe flag turned
-  down by default.
+- The unsafe flag of the Refine.refine function and its variants has been
+  renamed and dualized into typecheck and has been made mandatory.
 
 ** Ltac API **
 
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index db69b08a20..8f96ac223f 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,14 +42,13 @@ goal holes thanks to the `Refine` module, and in particular to the
 `Refine.refine` primitive.
 
 ```ocaml
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
+(** In [refine typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (default is [true]) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 ```
 
 In a first approximation, we can think of `'a Sigma.run` as
-- 
cgit v1.2.3


From e36d139f6cb73d1e5021a77d38925b2879efda62 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 17:24:43 +0200
Subject: Revert "[travis] temporary UniMath overlay"

This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43.

Not necessary anymore since UniMath/UniMath#715 has been merged.
---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3adc319355..d7714274e7 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -13,8 +13,8 @@
 ########################################################################
 # UniMath
 ########################################################################
-: ${UniMath_CI_BRANCH:=coq_makefile2-fix}
-: ${UniMath_CI_GITURL:=https://github.com/maximedenes/UniMath.git}
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
 
 ########################################################################
 # Unicoq + Metacoq
-- 
cgit v1.2.3


From c70a21a1c522639138dbcfac53fb2ed96d731d98 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:05:04 +0200
Subject: [travis] fix CoLoR by inserting some Require Import FunInd

---
 dev/ci/ci-color.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 57f569858b..a0a4e0749d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C
 sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
 sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
 
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
-- 
cgit v1.2.3


From bba2186f781695db9d0987758119fde061499fbc Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:44:01 +0200
Subject: [travis] fix Software Foundation (one added Require Extraction)

---
 dev/ci/ci-sf.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
 
 
-- 
cgit v1.2.3


From 2470182ac4bded5c433c8f6bc77eb7b96576dc8d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 14:48:22 +0200
Subject: [travis] overlays for CompCert and VST (an extra Require Export
 FunInd)

---
 dev/ci/ci-user-overlay.sh | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 200d431bcb..62c245b4fe 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -47,3 +47,10 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums"
     Corn_CI_BRANCH=external-bignums
     Corn_CI_GITURL=https://github.com/letouzey/corn.git
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+    CompCert_CI_BRANCH=less_init_plugins
+    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+    VST_CI_BRANCH=less_init_plugins
+    VST_CI_GITURL=https://github.com/letouzey/VST.git
+fi
-- 
cgit v1.2.3


From bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 15:47:56 +0200
Subject: [travis] overlay for fiat-crypto (a Require Import FunInd)

---
 dev/ci/ci-user-overlay.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 62c245b4fe..2ecd40416f 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -53,4 +53,6 @@ if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins"
     CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
     VST_CI_BRANCH=less_init_plugins
     VST_CI_GITURL=https://github.com/letouzey/VST.git
+    fiat_crypto_CI_BRANCH=less_init_plugins
+    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
 fi
-- 
cgit v1.2.3


From f4cec75fe74ff3f66f401efab357cae79124d984 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Jun 2017 10:32:17 +0200
Subject: Temporary overlays because fewer plugins are loaded at startup.

---
 dev/ci/ci-basic-overlay.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 54db58c01f..b582921ecb 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -73,14 +73,14 @@
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: ${CompCert_CI_BRANCH:=less_init_plugins}
+: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
 
 ########################################################################
 # VST
 ########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: ${VST_CI_BRANCH:=less_init_plugins}
+: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git}
 
 ########################################################################
 # fiat_parsers
@@ -91,8 +91,8 @@
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
+: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
 ########################################################################
 # bedrock_src
-- 
cgit v1.2.3


From c5dabed1c1f33005fe942882ea0fcf008d52784a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jun 2017 11:45:45 +0200
Subject: Remove bedrock from test suite.

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.
---
 dev/ci/ci-basic-overlay.sh  | 12 ------------
 dev/ci/ci-bedrock-facade.sh | 10 ----------
 dev/ci/ci-bedrock-src.sh    | 10 ----------
 dev/ci/ci-user-overlay.sh   |  4 ----
 4 files changed, 36 deletions(-)
 delete mode 100755 dev/ci/ci-bedrock-facade.sh
 delete mode 100755 dev/ci/ci-bedrock-src.sh

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b0..0099e815f4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -94,18 +94,6 @@
 : ${fiat_crypto_CI_BRANCH:=less_init_plugins}
 : ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
-########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
 ########################################################################
 # formal-topology
 ########################################################################
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073f..0000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b3..0000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 2ecd40416f..b242ce3bd9 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -33,10 +33,6 @@ fi
 echo "DEBUG: ci-user-overlay.sh 0"
 if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
     echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
     fiat_parsers_CI_BRANCH=trunk__API
     fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
 fi
-- 
cgit v1.2.3


From 5b109c098a46e5083ba0cf98b5fe72312331770e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 15 Jun 2017 19:42:22 +0200
Subject: fix dev/base_include (thanks Zimmi48)

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index defea713d8..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,7 +233,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Coqloop
 let go = loop
-- 
cgit v1.2.3


From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sun, 21 May 2017 14:46:30 +0200
Subject: Squashed commit of the following:

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.
---
 dev/include         | 1 +
 dev/top_printers.ml | 1 +
 2 files changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/include b/dev/include
index 0f43f00729..4835b360db 100644
--- a/dev/include
+++ b/dev/include
@@ -41,6 +41,7 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* univ info *) ppuniverse_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6ae5125f6d..e902da0b19 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,6 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
+let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 dev/base_include    | 2 +-
 dev/include         | 2 +-
 dev/top_printers.ml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index f9af0696b1..98cf67256f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
+(*let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*)
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/dev/include b/dev/include
index 4835b360db..1d87456de7 100644
--- a/dev/include
+++ b/dev/include
@@ -41,7 +41,7 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ info *) ppuniverse_info;;
+#install_printer  (* univ info *) ppcumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e902da0b19..abf6db1b7f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,7 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c)
+let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
-- 
cgit v1.2.3


From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 14 Jun 2017 16:32:47 +0200
Subject: A short cleanup

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 98cf67256f..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-(*let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*)
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
-- 
cgit v1.2.3


From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 dev/base_include    | 2 --
 dev/include         | 3 ++-
 dev/top_printers.ml | 1 -
 dev/vm_printers.ml  | 1 -
 4 files changed, 2 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index f9af0696b1..8ee1cceb23 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -58,8 +58,6 @@
 
 (* Open main files *)
 
-open API
-open Grammar_API
 open Names
 open Term
 open Vars
diff --git a/dev/include b/dev/include
index 1d87456de7..31ae5da71a 100644
--- a/dev/include
+++ b/dev/include
@@ -41,7 +41,8 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ info *) ppcumulativity_info;;
+#install_printer  (* cumulativity info *) ppcumulativity_info;;
+#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index abf6db1b7f..ff575e432c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,7 +8,6 @@
 
 (* Printers for the ocaml toplevel. *)
 
-open API
 open Util
 open Pp
 open Names
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index be6b914b6b..afa94a63e0 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,4 +1,3 @@
-open API
 open Format
 open Term
 open Names
-- 
cgit v1.2.3


From d06af26e6cd93c6bb819b38573603a5e1121ed68 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 18:24:45 +0200
Subject: Each user overlay goes into its own file.

This will avoid stupid merge conflicts in the future.
---
 dev/ci/ci-common.sh                                |  4 +-
 dev/ci/ci-user-overlay.sh                          | 58 ----------------------
 .../user-overlays/00669-maximedenes-ssr-merge.sh   |  4 ++
 dev/ci/user-overlays/README.md                     | 14 ++++++
 4 files changed, 21 insertions(+), 59 deletions(-)
 delete mode 100644 dev/ci/ci-user-overlay.sh
 create mode 100644 dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
 create mode 100644 dev/ci/user-overlays/README.md

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f1e1515d41..5435e95885 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -18,7 +18,9 @@ ls "$COQBIN"
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-source ${ci_dir}/ci-user-overlay.sh
+for overlay in ${ci_dir}/user-overlays/*.sh; do
+  source ${overlay}
+done
 source ${ci_dir}/ci-basic-overlay.sh
 
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
deleted file mode 100644
index 2ecd40416f..0000000000
--- a/dev/ci/ci-user-overlay.sh
+++ /dev/null
@@ -1,58 +0,0 @@
-#!/usr/bin/env bash
-
-# Add user overlays here. You can use some logic to detect if you are
-# in your travis branch and conditionally enable the overlay.
-
-# Some useful Travis variables:
-# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
-#
-# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
-#   the name of the branch currently being built; whereas for builds
-#   triggered by a pull request this is the name of the branch
-#   targeted by the pull request (in many cases this will be master).
-#
-# - TRAVIS_COMMIT: The commit that the current build is testing.
-#
-# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
-#   a pull request, “false” if it’s not a pull request.
-#
-# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
-#   the name of the branch from which the PR originated. "" if the
-#   current job is a push build.
-
-echo $TRAVIS_PULL_REQUEST_BRANCH
-echo $TRAVIS_PULL_REQUEST
-echo $TRAVIS_BRANCH
-echo $TRAVIS_COMMIT
-
-if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
-    mathcomp_CI_BRANCH=ssr-merge
-    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
-fi
-
-echo "DEBUG: ci-user-overlay.sh 0"
-if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
-    echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    fiat_parsers_CI_BRANCH=trunk__API
-    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
-    math_classes_CI_BRANCH=external-bignums
-    math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
-    Corn_CI_BRANCH=external-bignums
-    Corn_CI_GITURL=https://github.com/letouzey/corn.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
-    CompCert_CI_BRANCH=less_init_plugins
-    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
-    VST_CI_BRANCH=less_init_plugins
-    VST_CI_GITURL=https://github.com/letouzey/VST.git
-    fiat_crypto_CI_BRANCH=less_init_plugins
-    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
-fi
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
new file mode 100644
index 0000000000..af4a96f4ae
--- /dev/null
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
new file mode 100644
index 0000000000..9146d3d521
--- /dev/null
+++ b/dev/ci/user-overlays/README.md
@@ -0,0 +1,14 @@
+# Add overlays for your pull requests in this directory
+
+An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+
+The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+
+Example: `00669-maximedenes-ssr-merge.sh` containing
+
+```
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
+```
-- 
cgit v1.2.3


From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 11:41:40 +0200
Subject: [ide] Add route_id parameter to query call.

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 ####.
---
 dev/doc/changes.txt     | 4 ++++
 dev/doc/xml-protocol.md | 9 +++++++--
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0728608f31..159be9a582 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -288,6 +288,10 @@ document type". This allows for a more uniform handling of printing
 
 - The legacy `Interp` call has been turned into a noop.
 
+- The `query` call has been modified, now it carries a mandatory
+  "route_id" integer parameter, that associated the result of such
+  query with its generated feedback.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 2ff82c6888..127b4a6d2d 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -308,15 +308,20 @@ CoqIDE typically sets `force` to `false`.
 
 -------------------------------
 
+### <a name="command-query">**Query(route_id: integer, query: string, stateId: integer)**</a>
+
+`routeId` can be used to distinguish the result of a particular query,
+`stateId` should be set to the state the query should be run.
 
-### <a name="command-query">**Query(query: string, stateId: integer)**</a>
-In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state.
 ```html
 <call val="Query">
+  <pair>
+    <route_id val="${routeId}"/>
   <pair>
     <string>${query}</string>
     <state_id val="${stateId}"/>
   </pair>
+  </pair>
 </call>
 ```
 #### *Returns*
-- 
cgit v1.2.3


From e9e8420df7a1799d9fcc86430c31a68820dc90c3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 22 Jun 2017 14:38:31 +0200
Subject: Add missing definition and fix #use include;; as suggested by
 @amintimany.

---
 dev/top_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ff575e432c..1be72759c9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,6 +215,7 @@ let ppuniverse_context_future c =
   let ctx = Future.force c in
     ppuniverse_context ctx
 let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
+let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
-- 
cgit v1.2.3