X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=e36a1290c949ed8bdc5549546228fb82efff9ea3;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=5cfda009c26bb564af3a45205860d931c320befb;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 5cfda009c..e36a1290c 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -64,26 +64,6 @@ let level_of_uri u =
   String.sub name 4 (String.length name - 4)
 ;;
 
-let destroy_nat =
-  let is_nat_URI = NUri.eq (NUri.uri_of_string
-  "cic:/matita/ng/arithmetics/nat/nat.ind") in
-  let is_zero = function
-    | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when
-       is_nat_URI uri -> true
-    | _ -> false
-  in
-  let is_succ = function
-    | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when
-       is_nat_URI uri -> true
-    | _ -> false
-  in
-  let rec aux acc = function
-    | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl
-    | t when is_zero t -> Some acc
-    | _ -> None
-  in
-   aux 0
-
 (* CODICE c&p da NCicPp *)
 let nast_of_cic0 status
  ~(idref:
@@ -139,29 +119,25 @@ let nast_of_cic0 status
            | NCic.Appl l -> NCic.Appl (l@args)
            | _ -> NCic.Appl (hd :: args)))
     | NCic.Appl args as t ->
-       (match destroy_nat t with
-         | Some n -> idref (Ast.Num (string_of_int n, -1))
-         | None ->
-            let args =
-             if not !Acic2content.hide_coercions then args
-             else
-              match
-               NCicCoercion.match_coercion status ~metasenv ~context ~subst t
-              with
-               | None -> args
-               | Some (_,sats,cpos) -> 
+       let args =
+        if not !Acic2content.hide_coercions then args
+        else
+         match
+          NCicCoercion.match_coercion status ~metasenv ~context ~subst t
+         with
+          | None -> args
+          | Some (_,sats,cpos) -> 
 (* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di
    argomenti da saltare, come prima! *)
-                  if cpos < List.length args - 1 then
-                   List.nth args (cpos + 1) ::
-                    try snd (HExtlib.split_nth (cpos+sats+2) args)
-                    with Failure _->[]
-                  else
-                   args
-            in
-             (match args with
-                 [arg] -> idref (k ~context arg)
-               | _ -> idref (Ast.Appl (List.map (k ~context) args))))
+             if cpos < List.length args - 1 then
+              List.nth args (cpos + 1) ::
+               try snd (HExtlib.split_nth (cpos+sats+2) args) with Failure _->[]
+             else
+              args
+       in
+        (match args with
+            [arg] -> idref (k ~context arg)
+          | _ -> idref (Ast.Appl (List.map (k ~context) args)))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
         let name = NUri.name_of_uri uri in
 (* CSC