added comment for zack

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index aa546d773ca7821f43aada14e2562831ce9e66fa..ee259877dc63f7cde0ec7ef6bb2a8f6664145ba6 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -22,6 +22,8 @@ let mk_type n =
      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+
 (* porcatissima *)
 type reference = Ref of NUri.uri * NReference.spec
 let reference_of_ouri u indinfo =
@@ -40,6 +42,16 @@ let strictify =
   | Fix l -> `Fix (Lazy.force l)
 ;;
 
+let count_vars vars =
+ List.length 
+  (List.filter (fun v -> 
+     match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
+        Cic.Variable (_,Some _,_,_,_) -> false
+      | Cic.Variable (_,None,_,_,_) -> true
+      | _ -> assert false) vars)
+;;
+
+
 (***** A function to restrict the context of a term getting rid of unsed
        variables *******)
 
@@ -621,7 +633,7 @@ let convert_term uri t =
         let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
-    | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
+    | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
     | Cic.Sort (Cic.Type u) -> 
           NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[] 
@@ -648,8 +660,8 @@ let convert_term uri t =
     | Cic.MutInd (curi, tyno, ens) -> 
        let is_inductive, lno =
         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-           Cic.InductiveDefinition ([],_,lno,_) -> true, lno
-         | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
+           Cic.InductiveDefinition ([],vars,lno,_) -> true, lno + count_vars vars
+         | Cic.InductiveDefinition ((_,b,_,_)::_,vars,lno,_) -> b, lno + count_vars vars
          | _ -> assert false
        in
         aux_ens k curi octx ctx n_fix uri ens
@@ -657,7 +669,7 @@ let convert_term uri t =
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
        let lno =
         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-           Cic.InductiveDefinition (_,_,lno,_) -> lno
+           Cic.InductiveDefinition (_,vars,lno,_) -> lno + count_vars vars
          | _ -> assert false
        in
        aux_ens k curi octx ctx n_fix uri ens
@@ -670,8 +682,8 @@ let convert_term uri t =
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
         let is_inductive,lno =
          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-            Cic.InductiveDefinition ([],_,lno,_) -> true, lno
-          | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
+            Cic.InductiveDefinition ([],vars,lno,_) -> true, lno + count_vars vars
+          | Cic.InductiveDefinition ((_,b,_,_)::_,vars,lno,_) -> b, lno + count_vars vars
           | _ -> assert false in
         let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
         let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
@@ -799,14 +811,7 @@ let convert_obj_aux uri = function
             (get_relevance ty, name, nty, cl)::itl, fix_ty @ fix_cl @ acc)
          itl ([],[])
      in
-     NCic.Inductive(ind, leftno + List.length 
-       (List.filter (fun v -> 
-          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
-             Cic.Variable (_,Some _,_,_,_) -> false
-           | Cic.Variable (_,None,_,_,_) -> true
-           | _ -> assert false)
-          vars)
-       , itl, (`Provided, `Regular)),
+     NCic.Inductive(ind, leftno + count_vars vars, itl, (`Provided, `Regular)),
      fix_itl
  | Cic.Variable _ 
  | Cic.CurrentProof _ -> assert false