3 files changed, 13 insertions, 21 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c542fd976a..b4e2160f4e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1072,13 +1072,6 @@ module Goal = struct
     end
     end
 
-  exception NotExactlyOneSubgoal
-  let _ = CErrors.register_handler begin function
-  | NotExactlyOneSubgoal ->
-      CErrors.user_err (Pp.str"Not exactly one subgoal.")
-  | _ -> raise CErrors.Unhandled
-  end
-
   let enter_one f =
     let open Proof in
     Comb.get >>= function
@@ -1090,7 +1083,7 @@ module Goal = struct
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
-    | _ -> tclZERO NotExactlyOneSubgoal
+    | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *)
 
   let goals =
     Pv.get >>= fun step ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index e98f59f0f9..530204501e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -498,7 +498,7 @@ module Goal : sig
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
-  (** an error otherwise. *)
+  (** a fatal error otherwise. *)
   val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
diff --git a/engine/universes.ml b/engine/universes.ml
index 28058aeed8..fc441fd0b4 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -282,28 +282,27 @@ let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
 let fresh_universe_instance ctx =
-  Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) 
-    (AUContext.instance ctx)
+  let init _ = new_univ_level (Global.current_dirpath ()) in
+  Instance.of_array (Array.init (AUContext.size ctx) init)
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, constraints
 
 let fresh_instance ctx =
   let ctx' = ref LSet.empty in
-  let inst = 
-    Instance.subst_fn (fun v -> 
-      let u = new_univ_level (Global.current_dirpath ()) in
-	ctx' := LSet.add u !ctx'; u) 
-      (AUContext.instance ctx)
+  let init _ =
+    let u = new_univ_level (Global.current_dirpath ()) in
+    ctx' := LSet.add u !ctx'; u
+  in
+  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
   in !ctx', inst
 
 let existing_instance ctx inst = 
   let () = 
-    let a1 = Instance.to_array inst 
-    and a2 = Instance.to_array (AUContext.instance ctx) in
-    let len1 = Array.length a1 and len2 = Array.length a2 in 
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx in
       if not (len1 == len2) then
 	CErrors.user_err ~hdr:"Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
@@ -317,7 +316,7 @@ let fresh_instance_from ctx inst =
     | Some inst -> existing_instance ctx inst
     | None -> fresh_instance ctx 
   in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, (ctx', constraints)
 
 let unsafe_instance_from ctx =