diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
commit | b98ae49d282f73343c1950e960f4b3bc7c28de70 (patch) | |
tree | 53114d948cc278ca0a98e0a19e0ca9282ee891cd /vernac/comFixpoint.ml | |
parent | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (diff) | |
parent | 40114382c04aafa1c8e1c156ca24a5ad1aa4b9fb (diff) |
Merge PR #7906: universes_of_constr don't include universes of monomorphic constants
Diffstat (limited to 'vernac/comFixpoint.ml')
-rw-r--r-- | vernac/comFixpoint.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |