aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comFixpoint.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-26 15:56:28 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-26 15:56:28 +0200
commitb98ae49d282f73343c1950e960f4b3bc7c28de70 (patch)
tree53114d948cc278ca0a98e0a19e0ca9282ee891cd /vernac/comFixpoint.ml
parent0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (diff)
parent40114382c04aafa1c8e1c156ca24a5ad1aa4b9fb (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.ml5
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