From 8ba5d01a92d5f8fe87c025002fb0bcca8ecef8bc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 13 Jun 2017 15:42:23 -0400
Subject: API: Hints.run_hint,Pfedit.current_proof_statement

Add them for fiat-parsers
---
 API/API.mli | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/API/API.mli b/API/API.mli
index 68fbda7c73..8df25bf922 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3947,6 +3947,8 @@ sig
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
 
+  val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
+
   (* Deprecated *)
   val delete_current_proof : unit -> unit
   [@@ocaml.deprecated "use Proof_global.discard_current"]
@@ -4367,6 +4369,8 @@ sig
   val pp_hints_path : hints_path -> Pp.std_ppcmds
   val glob_hints_path :
     Prelude.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+  val run_hint : hint ->
+    ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
   val typeclasses_db : hint_db_name
   val add_hints_init : (unit -> unit) -> unit
   val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit
-- 
cgit v1.2.3


From 1eb8035c2d8593017043bc4aa1ff2ff008c9d4a8 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 13 Jun 2017 15:37:19 -0400
Subject: Update fiat-parsers overlay

---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 0099e815f4..0de6f6b6b8 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -85,8 +85,8 @@
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=trunk__API}
-: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
 
 ########################################################################
 # fiat_crypto
-- 
cgit v1.2.3


From 04c65cdb71e069d656a5253c6c47155566e563c7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 15 Jun 2017 12:21:06 -0400
Subject: Remove ci-fiat-parsers from allowed_failures

It shouldn't be failing.
---
 .travis.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index e7082a9eeb..224dfe2f57 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -64,7 +64,6 @@ matrix:
   allow_failures:
   - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
   - env: TEST_TARGET="ci-geocoq"
-  - env: TEST_TARGET="ci-fiat-parsers"
 
   include:
     # Full Coq test-suite with two compilers
-- 
cgit v1.2.3