diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /vernac/comFixpoint.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
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) |