diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 19 |
4 files changed, 16 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b740e192a7..c530cbdeac 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -986,7 +986,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = i*) (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) - Evd.empty_evar_universe_context + Evd.empty lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 41f3a5a8bf..26706321b5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -278,7 +278,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty_evar_universe_context + (*FIXME*) Evd.empty new_principle_type hook ; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 832e933a71..e07bce69c9 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8014abf651..ca9f995f15 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1250,7 +1250,7 @@ let is_opaque_constant c = | Declarations.Undef _ -> true | Declarations.Def _ -> false -let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) let current_proof_name = get_current_proof_name () in let name = match goal_name with @@ -1276,7 +1276,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos let lid = ref [] in let h_num = ref (-1) in Proof_global.discard_all (); - build_proof Evd.empty_evar_universe_context + build_proof Evd.empty ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in tclTHENLIST @@ -1324,7 +1324,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos Lemmas.start_proof na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) - ctx gls_type + sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then @@ -1380,7 +1380,10 @@ let com_terminate start_proof ctx tclIDTAC tclIDTAC; try let sigma, new_goal_type = build_new_goal_type () in - open_new_goal start_proof (Evd.evar_universe_context sigma) + let sigma = + Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env + in + open_new_goal start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); @@ -1416,11 +1419,14 @@ let (com_eqn : int -> Id.t -> | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant") in let (evmap, env) = Lemmas.get_current_context() in + let evmap = + Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env + in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - (Evd.evar_universe_context evmap) + evmap equation_lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1488,7 +1494,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let ctx = Evd.evar_universe_context evm in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = @@ -1542,5 +1547,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - ctx (Lemmas.mk_hook hook)) + evm (Lemmas.mk_hook hook)) () |