diff options
| -rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 3 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
9 files changed, 5 insertions, 16 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4d6f7b21f..26d252726 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1792,7 +1792,7 @@ let destructure_hyps = in let hyps = Proofview.Goal.hyps gl in try (* type_of can raise exceptions *) - loop (Environ.named_context_of_val hyps) + loop hyps with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bdddf310d..823082ace 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -686,7 +686,7 @@ module Goal = struct let env { env=env } = env let sigma { sigma=sigma } = sigma - let hyps { hyps=hyps } = hyps + let hyps { hyps=hyps } = Environ.named_context_of_val hyps let concl { concl=concl } = concl let lift s = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index c9296e694..0504efea5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -288,7 +288,7 @@ module Goal : sig type t val concl : t -> Term.constr - val hyps : t -> Environ.named_context_val + val hyps : t -> Context.named_context val env : t -> Environ.env val sigma : t -> Evd.evar_map diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4928ffcfe..ae0d1039b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -215,7 +215,6 @@ module New = struct let pf_global id gl = let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in Constrintern.construct_reference hyps id @@ -225,7 +224,6 @@ module New = struct let pf_ids_of_hyps gl = let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in ids_of_named_context hyps let pf_get_new_id id gl = @@ -234,7 +232,6 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in let sign = try Context.lookup_named id hyps with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id)) @@ -252,6 +249,6 @@ module New = struct let pf_last_hyp gl = let hyps = Proofview.Goal.hyps gl in - List.hd (Environ.named_context_of_val hyps) + List.hd hyps end diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b5c496e26..19e5906f8 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -46,7 +46,7 @@ let filter_hyp f tac = | _::rest -> seek rest in Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in - seek (Environ.named_context_of_val hyps) + seek hyps end let contradiction_context = @@ -74,7 +74,6 @@ let contradiction_context = | _ -> seek_neg rest in let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in seek_neg hyps end diff --git a/tactics/equality.ml b/tactics/equality.ml index 14770af00..36cb55e5b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1545,7 +1545,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in - let hyps = Environ.named_context_of_val hyps in (* The set of hypotheses using x *) let depdecls = let test (id,_,c as dcl) = @@ -1587,7 +1586,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in let (_,xval,_) = Tacmach.New.pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else @@ -1686,7 +1684,6 @@ let rewrite_multi_assumption_cond cond_eq_term cl = in Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in arec hyps gl end diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 34ea3dc87..2c64b669c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1355,7 +1355,6 @@ and interp_match_goal ist lz lr lmr = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in let hyps = if lr then List.rev hyps else hyps in let concl = Proofview.Goal.concl gl in let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps = diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2131dc480..1b8cf531b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -534,7 +534,6 @@ module New = struct let nthDecl m gl = let hyps = Proofview.Goal.hyps gl in try - let hyps = Environ.named_context_of_val hyps in List.nth hyps (m-1) with Failure _ -> Errors.error "No such assumption." diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fd14dc938..2d1ba7756 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -431,7 +431,6 @@ let find_name loc decl x gl = match x with | IntroMustBe id -> (* When name is given, we allow to hide a global name *) let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in let ids_of_hyps = ids_of_named_context hyps in let id' = next_ident_away id ids_of_hyps in if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used."); @@ -1907,7 +1906,6 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in - let hyps = Environ.named_context_of_val hyps in let id = let t = match ty with Some t -> t | None -> typ_of env sigmac c in let x = id_of_name_using_hdchar (Global.env()) t name in |