From 2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Jul 2017 23:51:52 +0200
Subject: Fix TypeclassDebug.out after conflicting PR merges

---
 test-suite/output/TypeclassDebug.out | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 73369ab713..8b38fe0ff4 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -1,18 +1,18 @@
 Debug: 1: looking for foo without backtracking
 Debug: 1.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2 : foo
-Debug: 1.1-2: looking for foo without backtracking
-Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2 : foo
-Debug: 1.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo
+Debug: 1.1-1 : foo
+Debug: 1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1 : foo
+Debug: 1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
 Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.
-- 
cgit v1.2.3


From df49e6b29fa9e8ac971c3e08f20ae6cb0f5b9889 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Jul 2017 00:01:26 +0200
Subject: [api] Fix base_include LTAC parts.

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/base_include b/dev/base_include
index bfbf6bb5d8..79ecd73e0d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -194,8 +194,8 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
-- 
cgit v1.2.3