From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: Changement des named_context Ajout de cast indiquant au kernel la
 strategie a suivre Resolution du bug sur les coinductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/tactic_printer.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'parsing/tactic_printer.ml')

diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 942bce7987..6b5b35dd2a 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -53,12 +53,13 @@ let thin_sign osign sign =
        try 
 	 if Sign.lookup_named id osign = (id,c,ty) then sign
 	 else raise Different
-       with Not_found | Different -> add_named_decl d sign)
-    sign ~init:empty_named_context
+       with Not_found | Different -> Environ.push_named_context_val d sign)
+    sign ~init:Environ.empty_named_context_val
 
 let rec print_proof sigma osign pf =
   let {evar_hyps=hyps; evar_concl=cl; 
        evar_body=body} = pf.goal in
+  let hyps = Environ.named_context_of_val hyps in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
@@ -78,6 +79,7 @@ let pr_change gl =
 
 let rec print_script nochange sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  let sign = Environ.named_context_of_val sign in
   match pf.ref with
     | None ->
         (if nochange then 
@@ -124,10 +126,12 @@ let rec print_info_script sigma osign pf =
 		   (str "." ++ fnl ())
                  else 
 		   (str";" ++ brk(1,3) ++
-		      print_info_script sigma sign pf1)
+		      print_info_script sigma 
+		      (Environ.named_context_of_val sign) pf1)
              | _ -> (str"." ++ fnl () ++
                        prlist_with_sep pr_fnl
-                         (print_info_script sigma sign) spfl))
+                         (print_info_script sigma 
+			    (Environ.named_context_of_val sign)) spfl))
 
 let format_print_info_script sigma osign pf = 
   hov 0 (print_info_script sigma osign pf)
-- 
cgit v1.2.3