X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_acic%2FdoubleTypeInference.ml;h=30a8f5c290fdaac79a3ecc28f10269f2d2db611f;hb=d3e3b22ce9cca9e4ca80f75a6bdc4c2df93efb0b;hp=98d12ceca9446e7c6550e1625d2938c38d22d60b;hpb=afa05d30f20de12e031c3e5c3e5c33c19c42a7d8;p=helm.git diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml index 98d12ceca..30a8f5c29 100644 --- a/helm/ocaml/cic_acic/doubleTypeInference.ml +++ b/helm/ocaml/cic_acic/doubleTypeInference.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception Impossible of int;; exception NotWellTyped of string;; exception WrongUriToConstant of string;; @@ -84,9 +86,6 @@ let rec does_not_occur n = | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur n ty && @@ -95,9 +94,6 @@ let rec does_not_occur n = | C.CoFix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur n ty &&