From 05dff3bdaaf474e67b0878bc2dd0952427ce277e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 22 Jun 2018 16:09:23 +0200 Subject: universes_of_constr don't include universes of monomorphic constants Apparently it was not useful. I don't remember what I was thinking when I added it. --- vernac/comFixpoint.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1d1cc62de..37258c2d4 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let env = Global.env () in - let vars = Univops.universes_of_constr env (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in -- cgit v1.2.3