From c694b91bba898aad1e071d91fa70b7c5574cbf98 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 17:42:53 +0200
Subject: Fix bug 4969, autoapply was not tagging shelved subgoals correctly as
 unresolvable

---
 tactics/class_tactics.ml      | 12 +++++++++---
 test-suite/bugs/closed/4969.v | 11 +++++++++++
 2 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/4969.v

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8d6c085e63..c5b0e149a8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1511,10 +1511,16 @@ let is_ground c gl =
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
+  let open Proofview.Notations in
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
-    ((c,cty,Univ.ContextSet.empty),0,ce) } in
-  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
+  let enter gl =
+    (unify_e_resolve false flags).enter gl
+                                 ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+      Proofview.tclEVARMAP >>= (fun sigma ->
+      let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+      Proofview.Unsafe.tclEVARS sigma)
+  in
+  Proofview.V82.of_tactic (Proofview.Goal.nf_enter { enter }) gl
diff --git a/test-suite/bugs/closed/4969.v b/test-suite/bugs/closed/4969.v
new file mode 100644
index 0000000000..4dee41e221
--- /dev/null
+++ b/test-suite/bugs/closed/4969.v
@@ -0,0 +1,11 @@
+Require Import Classes.Init.
+
+Class C A := c : A.
+Instance nat_C : C nat := 0.
+Instance bool_C : C bool := true.
+Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
+Proof. auto. Qed.
+
+Goal True.
+  class_apply @silly; [reflexivity|].
+  reflexivity. Fail Qed.
-- 
cgit v1.2.3


From 55cb913f029308e97bd262fc18d4338f404e7561 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 14 Feb 2017 12:35:39 +0100
Subject: don't require printing-only notation to be productive

---
 parsing/g_prim.ml4             |  5 ++++-
 parsing/g_vernac.ml4           |  2 +-
 parsing/pcoq.ml                |  1 +
 parsing/pcoq.mli               |  1 +
 test-suite/success/Notations.v |  4 ++++
 toplevel/metasyntax.ml         | 13 +++++++------
 6 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b90e06cd3e..a38043d0c0 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -34,7 +34,7 @@ GEXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string pattern_ident pattern_identref by_notation smart_global;
+    ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
@@ -106,6 +106,9 @@ GEXTEND Gram
   string:
     [ [ s = STRING -> s ] ]
   ;
+  lstring:
+    [ [ s = string -> (!@loc, s) ] ]
+  ;
   integer:
     [ [ i = INT      -> my_int_of_string (!@loc) i
       | "-"; i = INT -> - my_int_of_string (!@loc) i ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e61be53a99..0c4dbcc8d5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1122,7 +1122,7 @@ GEXTEND Gram
 	 idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            VernacSyntacticDefinition
 	     (id,(idl,c),local,b)
-     | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":=";
+     | IDENT "Notation"; local = obsolete_locality; s = lstring; ":=";
 	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 7dc02190ea..007a6c767f 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -267,6 +267,7 @@ module Prim =
     let integer = gec_gen "integer"
     let bigint = Gram.entry_create "Prim.bigint"
     let string = gec_gen "string"
+    let lstring = Gram.entry_create "Prim.lstring"
     let reference = make_gen_entry uprim "reference"
     let by_notation = Gram.entry_create "by_notation"
     let smart_global = Gram.entry_create "smart_global"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 37165f6ceb..fc1727fc1c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -137,6 +137,7 @@ module Prim :
     val bigint : Bigint.bigint Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
+    val lstring : string located Gram.entry
     val qualid : qualid located Gram.entry
     val fullyqualid : Id.t list located Gram.entry
     val reference : reference Gram.entry
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 07bbb60c40..32baeaa570 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -128,3 +128,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
+(* Check that we can have notations without any symbol iff they are "only printing". *)
+Fail Notation "" := (@nil).
+Notation "" := (@nil) (only printing).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 008d5cf9f5..ccb9c99d78 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -903,8 +903,8 @@ let find_precedence lev etyps symbols =
   let first_symbol =
     let rec aux = function
       | Break _ :: t -> aux t
-      | h :: t -> h
-      | [] -> assert false (* rule is known to be productive *) in
+      | h :: t -> Some h
+      | [] -> None in
     aux symbols in
   let last_is_terminal () =
     let rec aux b = function
@@ -914,7 +914,8 @@ let find_precedence lev etyps symbols =
       | [] -> b in
     aux false symbols in
   match first_symbol with
-  | NonTerminal x ->
+  | None -> [],0
+  | Some (NonTerminal x) ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
@@ -937,11 +938,11 @@ let find_precedence lev etyps symbols =
 	if Option.is_empty lev then
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
-  | Terminal _ when last_is_terminal () ->
+  | Some (Terminal _) when last_is_terminal () ->
       if Option.is_empty lev then
 	([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
-  | _ ->
+  | Some _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
       [],Option.get lev
 
@@ -991,7 +992,7 @@ let compute_syntax_data df modifiers =
   let symbols' = remove_curly_brackets symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
   let ntn_for_grammar = make_notation_key symbols' in
-  check_rule_productivity symbols';
+  if not onlyprint then check_rule_productivity symbols';
   let msgs,n = find_precedence n etyps symbols' in
   let innerlevel = NumLevel 200 in
   let typs =
-- 
cgit v1.2.3


From 8ce49dd1b436a17c4ee29c2893133829daac75f0 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 14 Feb 2017 12:36:15 +0100
Subject: reject notations that are both 'only printing' and 'only parsing'

---
 test-suite/success/Notations.v | 3 +++
 toplevel/metasyntax.ml         | 1 +
 2 files changed, 4 insertions(+)

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 32baeaa570..52acad7460 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -132,3 +132,6 @@ Qed.
 (* Check that we can have notations without any symbol iff they are "only printing". *)
 Fail Notation "" := (@nil).
 Notation "" := (@nil) (only printing).
+
+(* Check that a notation cannot be neither parsing nor printing. *)
+Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ccb9c99d78..e90d638d03 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -984,6 +984,7 @@ let remove_curly_brackets l =
 
 let compute_syntax_data df modifiers =
   let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in
+  if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
   let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
   let toks = split_notation_string df in
   let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
-- 
cgit v1.2.3


From dda3c644e195de2f72a81a0e2fb17e5095ea80ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Mar 2017 18:25:43 +0100
Subject: [travis] Backport trunk's travis support.

---
 .travis.yml               | 119 ++++++++++++++++++++++++++++++++++++++++++++++
 Makefile                  |   5 ++
 Makefile.ci               |  11 +++++
 dev/ci/ci-color.sh        |   8 ++++
 dev/ci/ci-common.sh       |  52 ++++++++++++++++++++
 dev/ci/ci-compcert.sh     |  13 +++++
 dev/ci/ci-coquelicot.sh   |  12 +++++
 dev/ci/ci-cpdt.sh         |  10 ++++
 dev/ci/ci-fiat-crypto.sh  |   9 ++++
 dev/ci/ci-flocq.sh        |   9 ++++
 dev/ci/ci-geocoq.sh       |  16 +++++++
 dev/ci/ci-hott.sh         |   8 ++++
 dev/ci/ci-iris-coq.sh     |  17 +++++++
 dev/ci/ci-math-classes.sh |  12 +++++
 dev/ci/ci-math-comp.sh    |  13 +++++
 dev/ci/ci-metacoq.sh      |  16 +++++++
 dev/ci/ci-sf.sh           |  11 +++++
 dev/ci/ci-tlc.sh          |   8 ++++
 dev/ci/ci-unimath.sh      |  15 ++++++
 19 files changed, 364 insertions(+)
 create mode 100644 .travis.yml
 create mode 100644 Makefile.ci
 create mode 100755 dev/ci/ci-color.sh
 create mode 100644 dev/ci/ci-common.sh
 create mode 100755 dev/ci/ci-compcert.sh
 create mode 100755 dev/ci/ci-coquelicot.sh
 create mode 100755 dev/ci/ci-cpdt.sh
 create mode 100755 dev/ci/ci-fiat-crypto.sh
 create mode 100755 dev/ci/ci-flocq.sh
 create mode 100755 dev/ci/ci-geocoq.sh
 create mode 100755 dev/ci/ci-hott.sh
 create mode 100755 dev/ci/ci-iris-coq.sh
 create mode 100755 dev/ci/ci-math-classes.sh
 create mode 100755 dev/ci/ci-math-comp.sh
 create mode 100755 dev/ci/ci-metacoq.sh
 create mode 100755 dev/ci/ci-sf.sh
 create mode 100755 dev/ci/ci-tlc.sh
 create mode 100755 dev/ci/ci-unimath.sh

diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 0000000000..de16f2d0b4
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,119 @@
+dist: trusty
+sudo: required
+# Until Ocaml becomes a language, we set a known one.
+language: c
+cache:
+  apt: true
+  directories:
+  - $HOME/.opam
+addons:
+  apt:
+    sources:
+    - avsm
+    packages:
+    - opam
+    - aspcud
+    - gcc-multilib
+env:
+  global:
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
+  # Main test suites
+  matrix:
+  - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+  - TEST_TARGET="validate"                           TW="travis_wait"
+  - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
+  - TEST_TARGET="ci-color"
+  - TEST_TARGET="ci-compcert"
+  - TEST_TARGET="ci-coquelicot"
+  - TEST_TARGET="ci-cpdt"
+  - TEST_TARGET="ci-geocoq"
+  - TEST_TARGET="ci-fiat-crypto"
+  - TEST_TARGET="ci-flocq"
+  - TEST_TARGET="ci-hott"
+  - TEST_TARGET="ci-iris-coq"
+  - TEST_TARGET="ci-math-classes"
+  - TEST_TARGET="ci-math-comp"
+  - TEST_TARGET="ci-sf"
+  - TEST_TARGET="ci-unimath"
+  # Not ready yet for 8.7
+  # - TEST_TARGET="ci-metacoq"
+  # - TEST_TARGET="ci-tlc"
+
+matrix:
+
+  allow_failures:
+  - env: TEST_TARGET="ci-cpdt"
+
+  # Full Coq test-suite with two compilers
+  # [TODO: use yaml refs and avoid duplication for packages list]
+  include:
+    - env:
+      - TEST_TARGET="test-suite"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+    - env:
+      - TEST_TARGET="test-suite"
+      - COMPILER="4.04.0"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+
+install:
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- eval $(opam config env)
+- opam config var root
+- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
+- opam list
+
+script:
+
+- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
+- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
+- echo -en 'travis_fold:end:coq.config\\r'
+
+- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
+- make -j ${NJOBS}
+- echo -en 'travis_fold:end:coq.build\\r'
+
+- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
+- ${TW} make -j ${NJOBS} ${TEST_TARGET}
+- echo -en 'travis_fold:end:coq.test\\r'
diff --git a/Makefile b/Makefile
index 1dd4efca2e..e84d5e3775 100644
--- a/Makefile
+++ b/Makefile
@@ -245,6 +245,11 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex 
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
+###########################################################################
+# Continuous Intregration Tests
+###########################################################################
+include Makefile.ci
+
 ###########################################################################
 # Emacs tags
 ###########################################################################
diff --git a/Makefile.ci b/Makefile.ci
new file mode 100644
index 0000000000..e4b5832f60
--- /dev/null
+++ b/Makefile.ci
@@ -0,0 +1,11 @@
+CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
+           ci-color ci-math-classes ci-tlc ci-fiat-crypto \
+           ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
+           ci-unimath
+
+.PHONY: $(CI_TARGETS)
+
+# Generic rule, we use make to easy travis integraton with mixed rules
+$(CI_TARGETS): ci-%:
+	./dev/ci/ci-$*.sh
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
new file mode 100755
index 0000000000..78ae7f02f9
--- /dev/null
+++ b/dev/ci/ci-color.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+
+( cd color && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
new file mode 100644
index 0000000000..412da626fd
--- /dev/null
+++ b/dev/ci/ci-common.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+
+set -xe
+
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
+export PATH=`pwd`/bin:$PATH
+
+ls `pwd`/bin
+
+# Maybe we should just use Ruby...
+mathcomp_CI_BRANCH=master
+mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+
+# git_checkout branch
+git_checkout()
+{
+  local _BRANCH=${1}
+  local _URL=${2}
+  local _DEST=${3}
+
+  echo "Checking out ${_DEST}"
+  git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
+  ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+  checkout_mathcomp math-comp
+  ( cd math-comp/mathcomp            && \
+    sed -i.bak '/ssrtest/d'     Make && \
+    sed -i.bak '/odd_order/d'   Make && \
+    sed -i.bak '/all\/all.v/d'  Make && \
+    sed -i.bak '/character/d'   Make && \
+    sed -i.bak '/real_closed/d' Make && \
+    sed -i.bak '/solvable/d'    Make && \
+    sed -i.bak '/field/d'       Make && \
+    sed -i.bak '/fingroup/d'    Make && \
+    sed -i.bak '/algebra/d'     Make && \
+    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+  echo -en 'travis_fold:end:ssr.install\\r'
+
+}
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
new file mode 100755
index 0000000000..ec09389f8e
--- /dev/null
+++ b/dev/ci/ci-compcert.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+CompCert_CI_BRANCH=master
+CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+
+opam install -j ${NJOBS} -y menhir
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+
+# Patch to avoid the upper version limit
+( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
new file mode 100755
index 0000000000..94bd5e468f
--- /dev/null
+++ b/dev/ci/ci-coquelicot.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+install_ssreflect
+
+# Setup coquelicot
+git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+
+( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
new file mode 100755
index 0000000000..18d7561804
--- /dev/null
+++ b/dev/ci/ci-cpdt.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget http://adam.chlipala.net/cpdt/cpdt.tgz
+tar xvfz cpdt.tgz
+
+( cd cpdt && make clean && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
new file mode 100755
index 0000000000..c669195ddd
--- /dev/null
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
+
+( cd fiat-crypto && make -j ${NJOBS} )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
new file mode 100755
index 0000000000..345924e40a
--- /dev/null
+++ b/dev/ci/ci-flocq.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq
+
+( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
new file mode 100755
index 0000000000..ce870e52b5
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# XXX: replace by generic template
+GeoCoq_CI_BRANCH=master
+GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
+
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
+
+( cd GeoCoq                                               && \
+  ./configure.sh                                          && \
+  sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+  coq_makefile -f Make -o Makefile                        && \
+  make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
new file mode 100755
index 0000000000..0c07564c02
--- /dev/null
+++ b/dev/ci/ci-hott.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+
+( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
new file mode 100755
index 0000000000..c21af976f4
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+install_ssreflect
+
+# Setup stdpp
+git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp
+
+( cd coq-stdpp && make -j ${NJOBS} && make install )
+
+# Setup Iris
+git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
+
+( cd iris-coq && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
new file mode 100755
index 0000000000..4450dc0710
--- /dev/null
+++ b/dev/ci/ci-math-classes.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
+( cd math-classes && make -j ${NJOBS} && make install )
+
+git_checkout v8.6 https://github.com/c-corn/corn.git corn
+( cd corn         && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
new file mode 100755
index 0000000000..2eb150cb52
--- /dev/null
+++ b/dev/ci/ci-math-comp.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+checkout_mathcomp math-comp
+
+# odd_order takes too much time for travis.
+( cd math-comp/mathcomp                           && \
+  sed -i.bak '/PFsection/d'                  Make && \
+  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
+  make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..91a33695b0
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# MetaCoq + UniCoq
+
+git_checkout master https://github.com/unicoq/unicoq.git unicoq
+
+( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+
+git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+
+( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
new file mode 100755
index 0000000000..5e41211f1a
--- /dev/null
+++ b/dev/ci/ci-sf.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz
+tar xvfz sf.tgz
+
+( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
+
+
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
new file mode 100755
index 0000000000..b946324924
--- /dev/null
+++ b/dev/ci/ci-tlc.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+
+( cd tlc && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
new file mode 100755
index 0000000000..15e619acbb
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_BRANCH=master
+UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath
+
+( cd UniMath                                  && \
+  sed -i.bak '/Folds/d'              Makefile && \
+  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
+  make -j ${NJOBS} BUILD_COQ=no )
+
-- 
cgit v1.2.3


From 5ee6e1ac4782ce0c2fb45f3927d210d3f1207053 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Mar 2017 23:37:33 +0100
Subject: [ltac] Move dummy plugin to plugins folder.

This is needed to fix `Declare ML Module "ltac_plugin".
---
 Makefile.common                 | 5 +++--
 ltac/ltac.mllib                 | 1 -
 ltac/ltac_plugin.ml             | 0
 ltac/ltac_plugin.mli            | 0
 plugins/ltac/LtacDummy.v        | 2 ++
 plugins/ltac/ltac_dummy.ml      | 0
 plugins/ltac/ltac_dummy.mli     | 0
 plugins/ltac/ltac_plugin.mlpack | 1 +
 plugins/ltac/vo.itarget         | 1 +
 9 files changed, 7 insertions(+), 3 deletions(-)
 delete mode 100644 ltac/ltac_plugin.ml
 delete mode 100644 ltac/ltac_plugin.mli
 create mode 100644 plugins/ltac/LtacDummy.v
 create mode 100644 plugins/ltac/ltac_dummy.ml
 create mode 100644 plugins/ltac/ltac_dummy.mli
 create mode 100644 plugins/ltac/ltac_plugin.mlpack
 create mode 100644 plugins/ltac/vo.itarget

diff --git a/Makefile.common b/Makefile.common
index 49fe1fd939..a2b59a93b2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -62,7 +62,7 @@ PLUGINDIRS:=\
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          decl_mode	btauto \
-  ssrmatching
+  ssrmatching   ltac
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
@@ -120,6 +120,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         string_syntax_plugin.cmo )
 DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
 DERIVECMO:=plugins/derive/derive_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 
 PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
@@ -127,7 +128,7 @@ PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
         $(FOURIERCMO) $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index 974943ddd6..fc51e48ae4 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -20,4 +20,3 @@ G_rewrite
 Tauto
 G_eqdecide
 G_ltac
-Ltac_plugin
diff --git a/ltac/ltac_plugin.ml b/ltac/ltac_plugin.ml
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/ltac/ltac_plugin.mli b/ltac/ltac_plugin.mli
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/plugins/ltac/LtacDummy.v b/plugins/ltac/LtacDummy.v
new file mode 100644
index 0000000000..4f96bbaeb9
--- /dev/null
+++ b/plugins/ltac/LtacDummy.v
@@ -0,0 +1,2 @@
+(* The sole reason of this file is to trick coq's build system to build the dummy ltac plugin *)
+Declare ML Module "ltac_plugin".
diff --git a/plugins/ltac/ltac_dummy.ml b/plugins/ltac/ltac_dummy.ml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/plugins/ltac/ltac_dummy.mli b/plugins/ltac/ltac_dummy.mli
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
new file mode 100644
index 0000000000..6efb477cce
--- /dev/null
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -0,0 +1 @@
+Ltac_dummy
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
new file mode 100644
index 0000000000..4eff76566a
--- /dev/null
+++ b/plugins/ltac/vo.itarget
@@ -0,0 +1 @@
+LtacDummy.vo
-- 
cgit v1.2.3


From d30d5a9b32e020586d265f8e879c287269c17575 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 6 Mar 2017 16:33:47 +0100
Subject: [travis] Move GeoCoq to allow fail.

We need to agree a bit more with upstream.
---
 .travis.yml         | 4 ++--
 dev/ci/ci-geocoq.sh | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index de16f2d0b4..f609852bc3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -27,7 +27,6 @@ env:
   - TEST_TARGET="ci-color"
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coquelicot"
-  - TEST_TARGET="ci-cpdt"
   - TEST_TARGET="ci-geocoq"
   - TEST_TARGET="ci-fiat-crypto"
   - TEST_TARGET="ci-flocq"
@@ -38,13 +37,14 @@ env:
   - TEST_TARGET="ci-sf"
   - TEST_TARGET="ci-unimath"
   # Not ready yet for 8.7
+  # - TEST_TARGET="ci-cpdt"
   # - TEST_TARGET="ci-metacoq"
   # - TEST_TARGET="ci-tlc"
 
 matrix:
 
   allow_failures:
-  - env: TEST_TARGET="ci-cpdt"
+  - env: TEST_TARGET="ci-geocoq"
 
   # Full Coq test-suite with two compilers
   # [TODO: use yaml refs and avoid duplication for packages list]
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index ce870e52b5..29667b018a 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -12,5 +12,7 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
 ( cd GeoCoq                                               && \
   ./configure.sh                                          && \
   sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+  sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
+  sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
   coq_makefile -f Make -o Makefile                        && \
   make -j ${NJOBS} )
-- 
cgit v1.2.3


From 53d30eb8b3186031658dafd74dc7ad012854f385 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva
Date: Wed, 8 Mar 2017 23:05:55 -0800
Subject: Fix #5132: coq_makefile generates incorrect install goal

---
 tools/coq_makefile.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a14..294575e0a5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -676,6 +676,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "VO=vo\n";
       print "VOFILES:=$(VFILES:.v=.$(VO))\n";
       classify_files_by_root "VOFILES" l inc;
+      classify_files_by_root "VFILES" l inc;
       print "GLOBFILES:=$(VFILES:.v=.glob)\n";
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
-- 
cgit v1.2.3


From 76c263b5eceac313ac2cdd3a3e7e2961876d3e31 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 20 Mar 2017 12:21:12 -0400
Subject: In the Kami project, that causes a stack overflow in one of the
 example files (ProcThreeStInl.v, when the final "Defined" runs). I've
 verified that the change here fixes the stack overflow there with Coq 8.5pl2.

In this version, all the recursive calls are in tail position. Instead of
taking a single list of instructions, `emit' here takes a curent list and a remaining
list of lists of instructions. That means the two calls elsewhere in the file now
add an empty list argument. The algorithm works on the current list until it's empty,
then works on the remaining lists. The most complex case is for Ksequence, where
one of the pieces becomes the new current list, and the other pieces are consed onto
the remaining sub-lists.
---
 kernel/cemitcodes.ml | 31 +++++++++++++++++--------------
 1 file changed, 17 insertions(+), 14 deletions(-)

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ad7a41a347..f13620e101 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -262,41 +262,44 @@ let emit_instr = function
   | Kstop ->
       out opSTOP
 
-(* Emission of a list of instructions. Include some peephole optimization. *)
+(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
 
-let rec emit = function
-  | [] -> ()
+let rec emit insns remaining = match insns with
+  | [] -> 
+     (match remaining with 
+       [] -> () 
+     | (first::rest) -> emit first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
       if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Kenvacc n :: c ->
       if n >= 1 && n <= 4
       then out(opPUSHENVACC1 + n - 1)
       else (out opPUSHENVACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Koffsetclosure ofs :: c ->
       if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
       else (out opPUSHOFFSETCLOSURE; out_int ofs);
-      emit c
+      emit c remaining
   | Kpush :: Kgetglobal id :: c ->
-      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c
+      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
   | Kpush :: Kconst (Const_b0 i) :: c ->
       if i >= 0 && i <= 3
       then out (opPUSHCONST0 + i)
       else (out opPUSHCONSTINT; out_int i);
-      emit c
+      emit c remaining
   | Kpush :: Kconst const :: c ->
       out opPUSHGETGLOBAL; slot_for_const const;
-      emit c
+      emit c remaining
   | Kpop n :: Kjump :: c ->
-      out opRETURN; out_int n; emit c
+      out opRETURN; out_int n; emit c remaining
   | Ksequence(c1,c2)::c ->
-      emit c1; emit c2;emit c
+      emit c1 (c2::c::remaining)
   (* Default case *)
   | instr :: c ->
-      emit_instr instr; emit c
+      emit_instr instr; emit c remaining
 
 (* Initialization *)
 
@@ -367,8 +370,8 @@ let repr_body_code = function
 
 let to_memory (init_code, fun_code, fv) =
   init();
-  emit init_code;
-  emit fun_code;
+  emit init_code [];
+  emit fun_code [];
   let code = String.create !out_position in
   String.unsafe_blit !out_buffer 0 code 0 !out_position;
   (** Later uses of this string are all purely functional *)
-- 
cgit v1.2.3