Made Proofview.Goal.hyps a named_context.

There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 1 insertions, 9 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b5c496e26d..19e5906f85 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 14770af005..36cb55e5b4 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 34ea3dc877..2c64b669c5 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 2131dc4807..1b8cf531bc 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 fd14dc9389..2d1ba7756c 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