diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 32 |
1 files changed, 15 insertions, 17 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0999b95d..5d41ec72 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,7 +115,7 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (pf_type_of gls c) + (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) = Anonymous)], GVar(d0,v_id)]) in - let body = fst (understand env Evd.empty glob_body)(*FIXME*) in + let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = @@ -305,7 +305,8 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then error ("check_not_nested : failure "^Id.to_string x) + then errorlabstrm "Recdef.check_not_nested" + (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -399,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = thin to_intros; h_intros to_intros; (fun g' -> - let ty_teq = pf_type_of g' (mkVar heq) in + let ty_teq = pf_unsafe_type_of g' (mkVar heq) in let teq_lhs,teq_rhs = let _,args = try destApp ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -513,13 +514,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app (pf_type_of g (mkVar id)) with + match decompose_app (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> eq_constr t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) @@ -654,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} let pf_type c tac gl = - let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in + let evars, ty = Typing.type_of (pf_env gl) (project gl) c in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl let pf_typel l tac = @@ -679,7 +680,7 @@ let mkDestructEq : if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_type_of g expr in + let type_of_expr = pf_unsafe_type_of g expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> @@ -1292,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in + let env = Global.env () in Proof_global.discard_all (); - build_proof Evd.empty + build_proof (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") @@ -1397,9 +1399,7 @@ let com_terminate start_proof ctx tclIDTAC tclIDTAC; try let sigma, new_goal_type = build_new_goal_type () in - let sigma = - Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env - in + let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in open_new_goal start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) @@ -1436,9 +1436,7 @@ 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 evmap = Evd.from_ctx (Evd.evar_universe_context evmap) 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) @@ -1511,12 +1509,12 @@ 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 functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (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 = fst (*FIXME*)(interp_constr env_with_pre_rec_args - Evd.empty + (Evd.from_env env_with_pre_rec_args) r) in let tcc_lemma_name = add_suffix function_name "_tcc" in |