From 90303e38d22479105927f0dd2fe95cce9447bd44 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 10 Aug 2016 11:26:30 +0200
Subject: Remove unused optional "predicative" argument.

---
 engine/evd.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 196f44760a..e4b174bcb3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -790,16 +790,16 @@ let merge_universe_subst evd subst =
 let with_context_set ?loc rigid d (a, ctx) =
   (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_level_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
-  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
+let new_sort_variable ?loc ?name rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name d in
     (d', Type u)
 
 let add_global_univ d u =
-- 
cgit v1.2.3


From 979b7cbba63f6c033bab40ad5c552572ab5d7d71 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 31 Jul 2016 07:57:13 +0200
Subject: Two protections against failures when printing evar_map.

Delimit the scope of the failure to ease potential need for debugging
the debugging printer.

Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
---
 engine/evd.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index e4b174bcb3..6ba8a51120 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1258,6 +1258,12 @@ let pr_instance_status (sc,typ) =
   | TypeProcessed -> str " [type is checked]"
   end
 
+let protect f x =
+  try f x
+  with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_constr a = protect print_constr a
+
 let pr_meta_map mmap =
   let pr_name = function
       Name id -> str"[" ++ pr_id id ++ str"]"
-- 
cgit v1.2.3