diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 05:44:46 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | dc03a4d9a7b527df0c2e571de55fd200666bdb11 (patch) | |
| tree | 7728d1f3a5d3bdf62ddee90ae60aa78e958c8d1e | |
| parent | ef8f09ef2fe338bb783591abb3cf8e6d5f4d404f (diff) | |
[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.
| -rw-r--r-- | vernac/declareObl.ml | 3 |
1 files changed, 0 insertions, 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 = |