From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 May 2018 17:44:34 +0200 Subject: Remove some occurrences of Evd.empty We address the easy ones, but they should probably be all removed. --- vernac/comFixpoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comFixpoint.ml') 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) -- cgit v1.2.3