12 files changed, 106 insertions, 26 deletions
diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
index 7b17e721b..7140a7c61 100644
--- a/dev/build/windows/MakeCoq_regtest_noproxy.bat
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -25,5 +25,5 @@ call MakeCoq_MinGW.bat ^
   -cygquiet=Y ^
   -destcyg   %ROOTPATH%\cygwin_coq64_85pl2_abs ^
   -destcoq   %ROOTPATH%\coq64_85pl2_abs
-
-pause
-\ No newline at end of file
+
+pause
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 0b61a31e7..16c972e80 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -40,4 +40,4 @@ if [ ! -f $donefile ] ; then
     echo unset OCAMLLIB >> $rcfile
 
     touch $donefile
-fi
-\ No newline at end of file
+fi
diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c
index 5e02c72bb..41f64f98b 100644
--- a/dev/build/windows/patches_coq/ln.c
+++ b/dev/build/windows/patches_coq/ln.c
@@ -134,4 +134,4 @@ int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLin
     
     // Everything is fine
     return 0;
-}
-\ No newline at end of file
+}
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index d66e2e7c4..cb1493d6a 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -86,7 +86,7 @@
 # VST
 ########################################################################
 : ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
 
 ########################################################################
 # fiat_parsers
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 5be8257e8..707adce30 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -24,6 +24,12 @@ passing `-bypass-API`.
 
 ### ML API
 
+General deprecation
+
+- All functions marked [@@ocaml.deprecated] in 8.7 have been
+  removed. Please, make sure your plugin is warning-free in 8.7 before
+  trying to port it over 8.8.
+
 We removed the following functions:
 
 - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
new file mode 100755
index 000000000..eb12bc227
--- /dev/null
+++ b/dev/lint-commits.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness for a range of commits
+
+CALLNAME="$0"
+
+function usage
+{
+    >&2 echo "usage: $CALLNAME <commit> <commit>"
+    >&2 echo "The order of commits is as given to 'git diff'"
+}
+
+if [ "$#" != 2 ];
+then
+    usage
+    exit 1
+fi
+
+BASE_COMMIT="$1"
+HEAD_COMMIT="$2"
+
+# git diff --check
+# uses .gitattributes to know what to check
+if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT";
+then
+    :
+else
+    >&2 echo "Whitespace errors!"
+    >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'."
+    >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
+    exit 1
+fi
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
new file mode 100755
index 000000000..ecf7880e2
--- /dev/null
+++ b/dev/lint-repository.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness over the repository.
+
+# lint-commits.sh seeks to prevent the worsening of already present
+# problems, such as tab indentation in ml files. lint-repository.sh
+# seeks to prevent the (re-)introduction of solved problems, such as
+# newlines at the end of .v files.
+
+CODE=0
+
+if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
+then
+    # Some problems are too widespread to fix in one commit, but we
+    # can still check that they don't worsen.
+    CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
+    PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
+    MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
+    dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1
+fi
+
+# Check that the files with 'whitespace' gitattribute end in a newline.
+# xargs exit status is 123 if any file failed the test
+find . "(" -path ./.git -prune ")" -type f \
+-o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \
+-print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1
+
+exit $CODE
diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh
index b8c1e5ee7..71a9162ef 100644
--- a/dev/nsis/FileAssociation.nsh
+++ b/dev/nsis/FileAssociation.nsh
@@ -187,4 +187,4 @@ NoOwn:
   !verbose pop
 !macroend
  
-!endif # !FileAssociation_INCLUDED
-\ No newline at end of file
+!endif # !FileAssociation_INCLUDED
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
new file mode 100755
index 000000000..1c578c05c
--- /dev/null
+++ b/dev/tools/check-eof-newline.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+if [ -z "$(tail -c 1 "$1")" ]
+then
+    exit 0
+else
+    echo "No newline at end of file $1!"
+    exit 1
+fi
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
new file mode 100755
index 000000000..8159506b4
--- /dev/null
+++ b/dev/tools/should-check-whitespace.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+# determine if a file has whitespace checking enabled in .gitattributes
+
+git check-attr whitespace -- "$1" | grep -q -v 'unspecified$'
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 70f7c4283..0d833d33b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -41,11 +41,11 @@ let pplab l = pp (pr_lab l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (ModPath.debug_to_string mp))
-let ppcon con = pp(debug_pr_con con)
-let ppproj con = pp(debug_pr_con (Projection.constant con))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
 let ppkn kn = pp(str (KerName.to_string kn))
-let ppmind kn = pp(debug_pr_mind kn)
-let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
@@ -125,10 +125,10 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
 let pP s = pp (hov 0 s)
 
 let safe_pr_global = function
-  | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
-  | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+  | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 			  int i ++ str ")")
-  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
 
@@ -226,7 +226,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x))
 
@@ -258,13 +258,13 @@ let constr_display csr =
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
   | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
-  | Const (c,u) -> "Const("^(string_of_con c)^","^(universes_display u)^")"
+  | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
-      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^","^(universes_display u)^")"
+      "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
   | Construct (((sp,i),j),u) ->
-      "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
+      "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
-  | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
+  | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display bl)^")"
@@ -432,7 +432,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_mind sp)
+      print_string (MutInd.debug_to_string sp)
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
@@ -441,7 +441,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_con sp)
+      print_string (Constant.debug_to_string sp)
 
   in
     try
@@ -503,7 +503,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun () -> in_current_context constr_display c)
+           (fun _ -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
@@ -519,7 +519,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun () -> in_current_context print_pure_constr c)
+           (fun _ -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index afa94a63e..8e43bf6ed 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,11 +10,11 @@ let ppripos (ri,pos) =
   | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
       print_string
-	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
+	("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
-      print_string ("getglob "^(string_of_con kn)^"\n"));
+      print_string ("getglob "^(Constant.to_string kn)^"\n"));
    print_flush ()
 
 let print_vfix () = print_string "vfix"
@@ -32,7 +32,7 @@ let print_idkey idk =
   match idk with
   | ConstKey sp ->
       print_string "Cons(";
-      print_string (string_of_con sp);
+      print_string (Constant.to_string sp);
       print_string ")"
   | VarKey id -> print_string (Id.to_string id)
   | RelKey i -> print_string "~";print_int i
@@ -63,7 +63,7 @@ and ppatom a =
   | Aid idk -> print_idkey idk
   | Atype u -> print_string "Type(...)"
   | Aind(sp,i) ->  print_string "Ind(";
-      print_string (string_of_mind sp);
+      print_string (MutInd.to_string sp);
       print_string ","; print_int i;
       print_string ")"