From dc03a4d9a7b527df0c2e571de55fd200666bdb11 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 05:44:46 -0400
Subject: [declareObl] Remove hack w.r.t. to universe normalization.

This was introduced in #6203 , but as far as I can see this
re-normalization step is not necessary.
---
 vernac/declareObl.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 4b5564129f..f9d842d6a7 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -517,9 +517,6 @@ let obligation_terminator entries uctx { name; num; auto } =
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (* Declare the obligation ourselves and drop the hook *)
     let prg = CEphemeron.get (ProgMap.find name !from_prg) in
-    (* Ensure universes are substituted properly in body and type *)
-    let body = EConstr.to_constr sigma (EConstr.of_constr body) in
-    let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
     let { obls; remaining=rem } = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
-- 
cgit v1.2.3