Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / gTopLevel / sequentPp.ml

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index bffb3030c27cc81b76693b7e1d83c3221697f3e0..df504e75a248f4a8fc5433681a9e90e33dd7adf3 100644 (file)
--- 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,20 +53,24 @@ 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 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
@@ -75,7 +81,7 @@ module XmlPp =
              (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
 ;;