5 files changed, 68 insertions, 3 deletions
diff --git a/test-suite/misc/11170.sh b/test-suite/misc/11170.sh
new file mode 100755
index 0000000000..da8843fcf6
--- /dev/null
+++ b/test-suite/misc/11170.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+set -e
+
+export PATH=$BIN:$PATH
+export OCAMLRUNPARAM=s=1
+
+${coqc#"$BIN"} misc/aux11170.v
diff --git a/test-suite/misc/aux11170.v b/test-suite/misc/aux11170.v
new file mode 100644
index 0000000000..d4a8630053
--- /dev/null
+++ b/test-suite/misc/aux11170.v
@@ -0,0 +1,6 @@
+Fixpoint T n := match n with O => nat | S n => nat -> T n end.
+Fixpoint app n : T n -> nat :=
+  match n with O => fun x => x | S n => fun f => app n (f 0) end.
+Definition n := (fix aux n := match n with S n => aux n + aux n | O => 1 end) 13.
+Axiom f : T n.
+Eval vm_compute in let t := (app n f, 0) in snd t.
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
new file mode 100755
index 0000000000..667d11f89e
--- /dev/null
+++ b/test-suite/misc/coq_environment.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+cat > coq_environment.txt <<EOT
+# we override COQLIB because we can
+COQLIB="$TMP/overridden" # bla bla
+OCAMLFIND="$TMP/overridden"
+FOOBAR="one more"
+EOT
+
+cp $BIN/coqc .
+cp $BIN/coq_makefile .
+mkdir -p overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+
+unset COQLIB
+N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo OCAMLFIND not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+./coq_makefile -o CoqMakefile -R . foo > /dev/null
+N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQMF_OCAMLFIND not overridden by coq_environment
+  cat CoqMakefile.conf
+  exit 1
+fi
+
+export COQLIB="/overridden2"
+N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by COQLIB when coq_environment present
+  coqc -config
+  exit 1
+fi
+
+rm -rf $TMP
+exit 0
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
index ba0bcb1b3c..0f843b3b14 100644
--- a/test-suite/misc/quotation_token/src/quotation.mlg
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram
   term: LEVEL "0"
     [ [ s = QUOTATION "foobar:" ->
         {
-          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
+          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ]
   ;
 END
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
index d89ab887a8..bb6eaff409 100644
--- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg
+++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
@@ -7,7 +7,7 @@ open Stdarg
 
 TACTIC EXTEND magic
 | [ "magic" ident(i) ident(j) ] -> {
-  let open Glob_term in
-  DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
+  let open Constrexpr in
+  DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
 }
 END