Merge ../kvx-work into kvx_fp_division

6 files changed, 12 insertions, 12 deletions

diff --git a/.gitattributes b/.gitattributes
index 02ab53c1..f30f2a66 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,3 +1,3 @@
 # Files that should be ignored by Github linguist
-test/* linguist-vendored
-doc/* linguist-documentation
+/test/** linguist-vendored
+/doc/** linguist-documentation
diff --git a/backend/IRC.ml b/backend/IRC.ml
index d9e4651e..21ee0799 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -906,10 +906,10 @@ let location_of_var g v =
 (* The exported interface *)
 
 let add_interf g v1 v2 =
-  addEdge g (nodeOfVar g v1) (nodeOfVar g v2)
+  let n1 = nodeOfVar g v1 in let n2 = nodeOfVar g v2 in addEdge g n1 n2
 
 let add_pref g v1 v2 =
-  addMovePref g (nodeOfVar g v1) (nodeOfVar g v2)
+  let n1 = nodeOfVar g v1 in let n2 = nodeOfVar g v2 in addMovePref g n1 n2
 
 let coloring g =
   initialNodePartition g;
diff --git a/common/Events.v b/common/Events.v
index 360da52f..7b16339a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -199,7 +199,7 @@ Next Obligation.
   elimtype False. elim NE. auto.
 Qed.
 Next Obligation.
-  red; intro. elim (H e). rewrite H0. auto.
+  red; intro; subst; intuition eauto.
 Qed.
 
 CoFixpoint traceinf_of_traceinf' (T': traceinf') : traceinf :=
diff --git a/common/Memory.v b/common/Memory.v
index e243d475..1e94d865 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -646,11 +646,11 @@ Next Obligation.
   apply access_max.
 Qed.
 Next Obligation.
-  specialize (nextblock_noaccess m b0 ofs k H0). intros.
+  exploit (nextblock_noaccess m b0 ofs k). auto. intros NOACC.
   rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
   destruct (zle lo ofs). destruct (zlt ofs hi).
-  assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto.
-  unfold perm in H2. rewrite H1 in H2. contradiction.
+  assert (P: perm m b ofs k Freeable) by auto using perm_cur.
+  unfold perm in P. rewrite NOACC in P. contradiction.
   auto. auto. auto.
 Qed.
 Next Obligation.
diff --git a/configure b/configure
index d71b4120..f99d1f50 100755
--- a/configure
+++ b/configure
@@ -541,14 +541,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1)
+  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1|8.15.0)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.1"
+            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.15.0"
             missingtools=true
         fi;;
   "")
diff --git a/lib/Intv.v b/lib/Intv.v
index 4b5ed77d..3a491819 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -245,8 +245,8 @@ Next Obligation.
   red. lia.
 Qed.
 Next Obligation.
-  assert (x = hi - 1 \/ x < hi - 1) by lia.
-  destruct H2. congruence. auto.
+  assert (EITHER: x = hi - 1 \/ x < hi - 1) by lia.
+  destruct EITHER. congruence. auto.
 Qed.
 Next Obligation.
   exists wildcard'; split; auto. lia.