From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 20 Jan 2005 10:32:01 +0000 (+0000)
Subject: - added rendering of constants/variable with/without body
X-Git-Tag: V_0_1_0~116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4356006cb7b5fef3acbb9de7fabe14481e675f2e;p=helm.git

- added rendering of constants/variable with/without body
---

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index c91eb200b..ef6999ca0 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -294,26 +294,28 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
 
 let build_decl_item seed id n s ~ids_to_inner_sorts =
  let module K = Content in
-  try
-   let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
-   if sort = "Prop" then
-      `Hypothesis
-        { K.dec_name = name_of n;
-          K.dec_id = gen_id declaration_prefix seed; 
-          K.dec_inductive = false;
-          K.dec_aref = id;
-          K.dec_type = s
-        }
-   else 
-      `Declaration
-        { K.dec_name = name_of n;
-          K.dec_id = gen_id declaration_prefix seed; 
-          K.dec_inductive = false;
-          K.dec_aref = id;
-          K.dec_type = s
-        }
-  with
-   Not_found -> assert false
+ let sort =
+   try
+    Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
+   with Not_found -> None
+ in
+ match sort with
+ | Some "Prop" ->
+    `Hypothesis
+      { K.dec_name = name_of n;
+        K.dec_id = gen_id declaration_prefix seed; 
+        K.dec_inductive = false;
+        K.dec_aref = id;
+        K.dec_type = s
+      }
+ | _ ->
+    `Declaration
+      { K.dec_name = name_of n;
+        K.dec_id = gen_id declaration_prefix seed; 
+        K.dec_inductive = false;
+        K.dec_aref = id;
+        K.dec_type = s
+      }
 ;;
 
 let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =