X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FgTopLevel%2FsequentPp.ml;h=c3ab41f8812ce0e94ad722fa9f235943f9a1a861;hb=d7e5adc6adcdcbc98964fa73b3d8e05cad428a6b;hp=bffb3030c27cc81b76693b7e1d83c3221697f3e0;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index bffb3030c..c3ab41f88 100644
--- a/helm/gTopLevel/sequentPp.ml
+++ b/helm/gTopLevel/sequentPp.ml
@@ -43,6 +43,8 @@ module XmlPp =
     let ids_to_father_ids = Hashtbl.create 503 in
     let ids_to_inner_sorts = Hashtbl.create 503 in
     let ids_to_inner_types = Hashtbl.create 503 in
+    let ids_to_hypotheses = Hashtbl.create 11 in
+    let hypotheses_seed = ref 0 in
     let seed = ref 0 in
      let acic_of_cic_context =
       Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
@@ -51,31 +53,35 @@ module XmlPp =
       let final_s,_ =
        (List.fold_right
          (fun binding (s,context) ->
-           match binding with
-              (Some (n,(Cic.Def t as b)) as entry)
-            | (Some (n,(Cic.Decl t as b)) as entry) ->
-               let acic = acic_of_cic_context context t in
-                [< s ;
-                   X.xml_nempty
-                    (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
-                    ["name",(match n with Cic.Name n -> n | _ -> assert false)]
-                    (Cic2Xml.print_term
-                      (UriManager.uri_of_string "cic:/dummy.con")
-                      ids_to_inner_sorts acic)
-                >], (entry::context)
-            | None ->
-               [< s ; X.xml_empty "Hidden" [] >], (None::context)
+           let hid = "h" ^ string_of_int !hypotheses_seed in
+            Hashtbl.add ids_to_hypotheses hid binding ;
+            incr hypotheses_seed ;
+            match binding with
+               (Some (n,(Cic.Def t as b)) as entry)
+             | (Some (n,(Cic.Decl t as b)) as entry) ->
+                let acic = acic_of_cic_context context t None in
+                 [< s ;
+                    X.xml_nempty
+                     (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
+                     ["name",(match n with Cic.Name n -> n | _ -> assert false);
+                      "id",hid]
+                     (Cic2Xml.print_term
+                       (UriManager.uri_of_string "cic:/dummy.con")
+                       ids_to_inner_sorts acic)
+                 >], (entry::context)
+             | None ->
+                [< s ; X.xml_empty "Hidden" [] >], (None::context)
          ) context ([<>],[])
        )
       in
-       let acic = acic_of_cic_context context goal in
+       let acic = acic_of_cic_context context goal None in
         X.xml_nempty "Sequent" ["no",string_of_int metano]
          [< final_s ;
             Xml.xml_nempty "Goal" []
              (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
                ids_to_inner_sorts acic)
          >],
-         ids_to_terms,ids_to_father_ids
+         ids_to_terms,ids_to_father_ids,ids_to_hypotheses
   ;;
  end
 ;;