- 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 c91eb200b3ed8a0f2ed63d675b6792ceafe1b95f..ef6999ca0887e65f5ad4036ca7320763d6693cda 100644 (file)
--- 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 =