Merge branch 'v8.6'

1 files changed, 10 insertions, 4 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 196f44760a..6ba8a51120 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 =
@@ -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"]"