summaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /plugins/funind/recdef.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r--plugins/funind/recdef.ml32
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