We do not compute inner-types for the metasenv ==> we handle it in a particular

way, always generating `Declaration and `Definition (instead of `Hypothesis and
`Proof when the sort is Prop).

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 82f0005f5eaf08af13187c769ba2323da61205e0..7996f927a0d222381dafc92c5abb882204361161 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -114,49 +114,49 @@ let test_for_lifting ~ids_to_inner_types =
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ALambda (id,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ALetIn (id,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.AAppl (id,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false) 
+          with Not_found -> false) 
     | C.AConst (id,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false) 
+          with Not_found -> false) 
     | C.AMutInd (id,_,_,_) -> false
     | C.AMutConstruct (id,_,_,_,_) -> 
        (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
         (* oppure: false *)
     | C.AMutCase (id,_,_,_,_,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.AFix (id,_,_) ->
           (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ACoFix (id,_,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
 ;;
 
 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
@@ -184,7 +184,7 @@ let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
                C.ARel (idr,idref,n,b) ->
                  let sort = 
                    (try Hashtbl.find ids_to_inner_sorts idr 
-                    with notfound -> "Type") in 
+                    with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     K.Premise 
                       { K.premise_id = gen_id seed;
@@ -282,7 +282,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
           K.conclude_args = [K.Term t];
           K.conclude_conclusion = 
               try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-              with notfound -> None
+              with Not_found -> None
         };
     }
 ;;
@@ -303,7 +303,7 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
           K.conclude_conclusion = 
             try Some 
              (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-            with notfound -> 
+            with Not_found -> 
               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
                  None -> None
               | Some t -> 
@@ -315,37 +315,43 @@ 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
-  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 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 seed; 
-         K.dec_inductive = false;
-         K.dec_aref = id;
-         K.dec_type = s
-       }
+  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 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 seed; 
+          K.dec_inductive = false;
+          K.dec_aref = id;
+          K.dec_type = s
+        }
+  with
+   Not_found -> assert false
 ;;
 
 let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
-  let sort = Hashtbl.find ids_to_inner_sorts id in
-  if sort = "Prop" then
-     `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
-  else 
-     `Definition
-       { K.def_name = name_of n;
-         K.def_id = gen_id seed; 
-         K.def_aref = id;
-         K.def_term = t
-       }
+  try
+   let sort = Hashtbl.find ids_to_inner_sorts id in
+   if sort = "Prop" then
+      `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+   else 
+      `Definition
+        { K.def_name = name_of n;
+          K.def_id = gen_id seed; 
+          K.def_aref = id;
+          K.def_term = t
+        }
+  with
+   Not_found -> assert false
 
 (* the following function must be called with an object of sort
 Prop. For debugging purposes this is tested again, possibly raising an 
@@ -445,7 +451,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                   K.conclude_conclusion = 
                      try Some 
                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                     with notfound -> None
+                     with Not_found -> None
                  };
             })
     | C.AConst (id,uri,exp_named_subst) as t ->
@@ -464,7 +470,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
         let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
         (match 
           (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
-           with notfound -> None)
+           with Not_found -> None)
          with
              Some tety -> (* we must lift up the argument *)
                let p = (aux te) in
@@ -480,7 +486,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                      K.conclude_conclusion = 
                        try Some 
                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with notfound -> None  
+                       with Not_found -> None  
                    }
                }
            | None ->
@@ -496,7 +502,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                      K.conclude_conclusion = 
                        try Some 
                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with notfound -> None 
+                       with Not_found -> None 
                    }
                }
          )  
@@ -521,7 +527,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
         }
     | C.AFix (id, no, funs) -> 
@@ -552,7 +558,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
         } 
     | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> 
@@ -576,7 +582,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
         } 
     | C.ACoFix (id,no,funs) -> 
@@ -607,7 +613,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                  with notfound -> None
+                  with Not_found -> None
               };
         } 
      in 
@@ -741,7 +747,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None  
+                   with Not_found -> None  
               }
           } 
   | _ -> raise NotApplicable
@@ -791,7 +797,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
           } 
       else raise NotApplicable
@@ -801,6 +807,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
 let map_conjectures
  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
 =
+ let module K = Content in
  let context' =
   List.map
    (function
@@ -808,13 +815,26 @@ let map_conjectures
      | (id,Some (name,Cic.ADecl t)) ->
          id,
           Some
-           (build_decl_item seed (get_id t) name t
-            ~ids_to_inner_sorts)
+           (* We should call build_decl_item, but we have not computed *)
+           (* the inner-types ==> we always produce a declaration      *)
+           (`Declaration
+             { K.dec_name = name_of name;
+               K.dec_id = gen_id seed; 
+               K.dec_inductive = false;
+               K.dec_aref = get_id t;
+               K.dec_type = t
+             })
      | (id,Some (name,Cic.ADef t)) ->
          id,
           Some
-           (build_def_item seed (get_id t) name t
-            ~ids_to_inner_sorts ~ids_to_inner_types)
+           (* We should call build_def_item, but we have not computed *)
+           (* the inner-types ==> we always produce a declaration     *)
+           (`Definition
+              { K.def_name = name_of name;
+                K.def_id = gen_id seed; 
+                K.def_aref = get_id t;
+                K.def_term = t
+              })
    ) context
  in
   (id,n,context',ty)