aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comFixpoint.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comFixpoint.ml')
-rw-r--r--vernac/comFixpoint.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 85c0699ea..d996443d6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -232,7 +232,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
- check_evars_are_solved env evd Evd.empty;
+ check_evars_are_solved env evd (Evd.from_env env);
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
check_mutuality env evd isfix (List.combine fixnames fixdefs)