diff options
| author | Maxime Dénès | 2019-04-05 12:18:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:45 +0200 |
| commit | 5af486406e366bf23558311a7367e573c617e078 (patch) | |
| tree | e2996582ca8eab104141dd75b82ac1777e53cb72 /vernac | |
| parent | f6dc8b19760aaf0cc14e6d9eb2d581ba1a05a762 (diff) | |
Remove calls to global env in Inductiveops
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/indschemes.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 1e733acc59..642695bda4 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -313,7 +313,9 @@ let warn_cannot_build_congruence = strbrk "Cannot build congruence scheme because eq is not found") let declare_congr_scheme ind = - if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin + let env = Global.env () in + let sigma = Evd.from_env env in + if Hipattern.is_equality_type env sigma (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with e when CErrors.noncritical e -> false |