ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index c7d59aedc6ce91803f496c8affa2b77c37cea8f2..72699f7e3cb2b584da6617a278a1b1f611945abd 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -122,7 +122,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
           with Not_found -> false) 
     | C.AMeta (id,_,_) -> 
          (try 
-            Hashtbl.find ids_to_inner_sorts id = "Prop"
+            Hashtbl.find ids_to_inner_sorts id = `Prop
           with Not_found -> assert false)
     | C.ASort (id,_) -> false
     | C.AImplicit _ -> raise NotImplemented
@@ -300,7 +300,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts =
    with Not_found -> None
  in
  match sort with
- | Some "Prop" ->
+ | Some `Prop ->
     `Hypothesis
       { K.dec_name = name_of n;
         K.dec_id = gen_id declaration_prefix seed; 
@@ -343,9 +343,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
             (match t with 
                C.ARel (idr,idref,n,b) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts idr 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts idr 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     K.Premise 
                       { K.premise_id = gen_id premise_prefix seed;
                         K.premise_xref = idr;
@@ -355,9 +356,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  else (K.Term t)
              | C.AConst(id,uri,[]) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts id 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     K.Lemma 
                       { K.lemma_id = gen_id lemma_prefix seed;
                         K.lemma_name = UriManager.name_of_uri uri;
@@ -366,9 +368,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  else (K.Term t)
              | C.AMutConstruct(id,uri,tyno,consno,[]) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts id 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
                         CicEnvironment.get_obj CicUniv.empty_ugraph uri
@@ -408,7 +411,7 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
-   if sort = "Prop" then
+   if sort = `Prop then
        (let p = 
         (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
        in 
@@ -436,17 +439,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
     match t with 
       C.ARel (id,idref,n,b) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.AVar (id,uri,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.AMeta (id,n,l) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.ASort (id,s) -> raise Not_a_proof
@@ -455,7 +458,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
     | C.ACast (id,v,t) -> aux v
     | C.ALambda (id,n,s,t) -> 
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = `Prop then 
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -475,7 +478,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -530,13 +533,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             })
     | C.AConst (id,uri,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
     | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = `Prop then 
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
@@ -728,9 +731,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   let idarg = get_id arg in
                   let sortarg = 
                     (try (Hashtbl.find ids_to_inner_sorts idarg)
-                     with Not_found -> "Type") in
+                     with Not_found -> `Type (CicUniv.fresh())) in
                   let hdarg = 
-                    if sortarg = "Prop" then
+                    if sortarg = `Prop then
                       let (co,bo) = 
                         let rec bc = 
                           function 
@@ -813,8 +816,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   else 
                     let aid = get_id a in
                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
-                      with Not_found -> "Type") in
-                    if asort = "Prop" then
+                      with Not_found -> `Type (CicUniv.fresh())) in
+                    if asort = `Prop then
                       K.ArgProof (aux a)
                     else K.Term a in
                 hd::(ma_aux (n-1) tl) in