7 files changed, 45 insertions, 16 deletions
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
@@ -95,6 +95,18 @@
 : ${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
 ########################################################################
 : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/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 )
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
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
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index f2314e224f..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 DeBrujin  -->
+<!-- The substitutions are ordered by increasing de Bruijn  -->
 <!-- index. An empty substitution means that that index is -->
 <!-- not accessible.                                       -->
 <!ELEMENT META (substitution*)>
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 474cc85c17..f8498c4023 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,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))
@@ -457,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")"
 
@@ -502,7 +492,6 @@ VERNAC COMMAND EXTEND PrintConstr
 END
 *)
 
-open Pcoq
 open Genarg
 open Stdarg
 open Egramml