From 5b109c098a46e5083ba0cf98b5fe72312331770e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 15 Jun 2017 19:42:22 +0200
Subject: fix dev/base_include (thanks Zimmi48)

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index defea713d8..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,7 +233,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Coqloop
 let go = loop
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index f9af0696b1..98cf67256f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ 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_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*)
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
-- 
cgit v1.2.3


From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 14 Jun 2017 16:32:47 +0200
Subject: A short cleanup

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 98cf67256f..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ 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_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
-- 
cgit v1.2.3


From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 dev/base_include | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index f9af0696b1..8ee1cceb23 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -58,8 +58,6 @@
 
 (* Open main files *)
 
-open API
-open Grammar_API
 open Names
 open Term
 open Vars
-- 
cgit v1.2.3