From b07f7a2ac4f23a29d1762b4f78fc1506925a5019 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Apr 2017 17:41:31 -0400
Subject: Add bedrock targets src and facade

---
 dev/ci/ci-basic-overlay.sh  | 13 ++++++++++++-
 dev/ci/ci-bedrock-facade.sh | 10 ++++++++++
 dev/ci/ci-bedrock-src.sh    | 10 ++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100755 dev/ci/ci-bedrock-facade.sh
 create 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 336ce9d8f1..e0851816ce 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -94,6 +94,18 @@
 : ${fiat_crypto_CI_BRANCH:=master}
 : ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
 
+########################################################################
+# bedrock_src
+########################################################################
+: ${bedrock_src_CI_BRANCH:=master}
+: ${bedrock_src_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
+
+########################################################################
+# bedrock_facade
+########################################################################
+: ${bedrock_facade_CI_BRANCH:=master}
+: ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
+
 ########################################################################
 # CoLoR
 ########################################################################
@@ -109,4 +121,3 @@
 ########################################################################
 : ${tlc_CI_BRANCH:=master}
 : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
-
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
new file mode 100755
index 0000000000..95cfa3073f
--- /dev/null
+++ b/dev/ci/ci-bedrock-facade.sh
@@ -0,0 +1,10 @@
+#!/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
new file mode 100755
index 0000000000..532611d4b3
--- /dev/null
+++ b/dev/ci/ci-bedrock-src.sh
@@ -0,0 +1,10 @@
+#!/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 )
-- 
cgit v1.2.3


From b4ca718e7cb62933ea39b61ed3737f3479517bdf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Apr 2017 15:07:37 +0200
Subject: Adding a dedicated travis overlay for fiat-parsers.

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

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index bb193ebb55..fad6472911 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,7 +25,7 @@ echo $TRAVIS_PULL_REQUEST
 echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
-if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then
-    mathcomp_CI_BRANCH=no_camlp4_compat
-    mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
+if [ $TRAVIS_PULL_REQUEST == "568" ] || [ $TRAVIS_BRANCH == "remove-tactic-compat" ]; then
+    fiat_parsers_CI_BRANCH=fix-ml
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat.git
 fi
-- 
cgit v1.2.3


From 6d4f2222aa7ff6039f9f386cbc38201a0cd60c08 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Apr 2017 17:21:14 +0200
Subject: Document the API changes.

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

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7f915b7819..8ea1638c99 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,15 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+** Tactic API **
+
+- pf_constr_of_global now returns a tactic instead of taking a continuation.
+  Thus it only generates one instance of the global reference, and it is the
+  caller's responsibility to perform a focus on the goal.
+
+- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
+  was very specific. Use tclPROGRESS instead.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
-- 
cgit v1.2.3


From 34d8de84ceb853c98bc80a0623f9afeae317d75f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:25:49 +0200
Subject: Locally disable some warnings.

---
 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 474cc85c17..918e98f778 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (* Printers for the ocaml toplevel. *)
+[@@@ocaml.warning "-32"]
 
 open Util
 open Pp
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

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

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 918e98f778..7caaf2d9d5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -503,7 +503,6 @@ VERNAC COMMAND EXTEND PrintConstr
 END
 *)
 
-open Pcoq
 open Genarg
 open Stdarg
 open Egramml
-- 
cgit v1.2.3


From 5365971dfdf4136586527aa4f4c85fbfebeee0bd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 15:00:56 +0200
Subject: Fix for bug 5507. Mispelt de Bruijn.

---
 dev/doc/cic.dtd | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index f2314e224f..7a9d7eb1e2 100644
--- a/dev/doc/cic.dtd
+++ b/dev/doc/cic.dtd
@@ -125,7 +125,7 @@
           id     ID     #REQUIRED
           sort   %sort; #REQUIRED>
 
-<!-- The substitutions are ordered by increasing DeBrujin  -->
+<!-- The substitutions are ordered by increasing DeBruijn  -->
 <!-- index. An empty substitution means that that index is -->
 <!-- not accessible.                                       -->
 <!ELEMENT META (substitution*)>
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 dev/doc/cic.dtd | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index 7a9d7eb1e2..cc33efd483 100644
--- a/dev/doc/cic.dtd
+++ b/dev/doc/cic.dtd
@@ -125,7 +125,7 @@
           id     ID     #REQUIRED
           sort   %sort; #REQUIRED>
 
-<!-- The substitutions are ordered by increasing DeBruijn  -->
+<!-- The substitutions are ordered by increasing de Bruijn  -->
 <!-- index. An empty substitution means that that index is -->
 <!-- not accessible.                                       -->
 <!ELEMENT META (substitution*)>
-- 
cgit v1.2.3


From 8dc2adfd102185c6c3c4b61709f2b55aefab2641 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 29 Apr 2017 13:07:45 -0400
Subject: Add bmsherman/topology to the ci

This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
---
 dev/ci/ci-basic-overlay.sh   |  6 ++++++
 dev/ci/ci-formal-topology.sh | 28 ++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100755 dev/ci/ci-formal-topology.sh

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e0851816ce..5da13c1008 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -106,6 +106,12 @@
 : ${bedrock_facade_CI_BRANCH:=master}
 : ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
 
+########################################################################
+# formal-topology
+########################################################################
+: ${formal_topology_CI_BRANCH:=ci}
+: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
+
 ########################################################################
 # CoLoR
 ########################################################################
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
new file mode 100755
index 0000000000..ecb36349fb
--- /dev/null
+++ b/dev/ci/ci-formal-topology.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
+
+Corn_CI_DIR=${CI_BUILD_DIR}/corn
+
+formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
+
+# Setup Math-Classes
+
+git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+
+( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup Corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup formal-topology
+
+git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
+
+( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} )
-- 
cgit v1.2.3


From 75a808f893a68eaf82296535e0d168e0f09f8193 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 8 May 2017 15:26:05 +0200
Subject: Fix warnings in top_printers

Note that [@@@ocaml.warning "-32"] caused an error with Drop.
It was put there because I didn't realise the warning was about a real issue.
---
 dev/top_printers.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7caaf2d9d5..f8498c4023 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (* Printers for the ocaml toplevel. *)
-[@@@ocaml.warning "-32"]
 
 open Util
 open Pp
@@ -60,14 +59,6 @@ let pprecarg = function
      str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
 let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 
-let pprecarg = function
-  | Declarations.Norec -> str "Norec"
-  | Declarations.Mrec (mind,i) ->
-     str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
-  | Declarations.Imbr (mind,i) ->
-     str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
-let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
-
 (* term printers *)
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
@@ -458,8 +449,6 @@ let print_pure_constr csr =
 	print_string (Printexc.to_string e);print_flush ();
 	raise e
 
-let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
-
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
-- 
cgit v1.2.3


From f1707b32c96931eb1c1d8153b8570234321153c2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 10 May 2017 17:23:24 -0400
Subject: Switch bedrock to mit-plv base

---
 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 5da13c1008..1dfade261f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -98,13 +98,13 @@
 # bedrock_src
 ########################################################################
 : ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
+: ${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/JasonGross/bedrock.git}
+: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # formal-topology
-- 
cgit v1.2.3


From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:30:09 +0200
Subject: Adding support for using grammar entries returning no value in
 EXTEND.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f8498c4023..ce6d5dff05 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
 
 let _ =
   try
@@ -526,7 +526,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3


From 2b00427c545be77805c6e954c2fa9c45682fec85 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 18 May 2017 14:07:04 -0400
Subject: Fix a typo

---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 52b158871b..98e80c7652 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1082,7 +1082,7 @@ function make_coq {
     copq_coq_gtk
     copy_coq_license
 
-    # make clean seems to br broken for 8.5pl2
+    # make clean seems to be broken for 8.5pl2
     # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
     # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
     # make clean
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 dev/v8-syntax/syntax-v8.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 64431ea161..fa2864cec9 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1158,7 +1158,7 @@ $$
 \nlsep \TERM{Abort}~\NT{ident}
 \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 \nlsep \TERM{Qed}
-\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
+\nlsep \TERM{Save}~\NT{ident}}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
 \nlsep \TERM{Suspend}
 \nlsep \TERM{Resume}~\OPT{\NT{ident}}
-- 
cgit v1.2.3