diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-21 20:47:32 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 07:31:44 +0200 |
| commit | 81b812c0512fb61342e3f43ebc29bf843a079321 (patch) | |
| tree | 518a3e81749db570b7fc1a65be19f1e586cf3ffe /plugins/funind/invfun.ml | |
| parent | 9f0f12e4aa2934283fd3fb3c61f977081cb99a3a (diff) | |
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 832e933a7..e07bce69c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1079,7 +1079,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_id = mk_correct_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty_evar_universe_context + (*FIXME*) Evd.empty (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by @@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty_evar_universe_context + (*FIXME*) Evd.empty (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by |