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
---
 contrib/xml/xmlcommand.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/xml/xmlcommand.ml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index e8f149402d..96f73abe0e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -290,7 +290,7 @@ let find_hyps t =
     | T.Meta _
     | T.Evar _
     | T.Sort _ -> l
-    | T.Cast (te,ty) -> aux (aux l te) ty
+    | T.Cast (te,_, ty) -> aux (aux l te) ty
     | T.Prod (_,s,t) -> aux (aux l s) t
     | T.Lambda (_,s,t) -> aux (aux l s) t
     | T.LetIn (_,s,_,t) -> aux (aux l s) t
@@ -359,7 +359,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
                (* t will not be exported to XML. Thus no unsharing performed *)
                final_var_ids,(n, Acic.Def  (Unshare.unshare b',t))::tl'
         in
-         aux [] (List.rev evar_hyps)
+         aux [] (List.rev (Environ.named_context_of_val evar_hyps))
        in
         (* We map the named context to a rel context and every Var to a Rel *)
         (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
-- 
cgit v1.2.3