ocaml 3.09 transition

[helm.git] / helm / fix_params / cicFindParameters.ml

diff --git a/helm/fix_params/cicFindParameters.ml b/helm/fix_params/cicFindParameters.ml
index 03c3e1c85be094463eff514d6e32f8f9752ef6d1..c78d8d21907e622fc1c7fd89fc1f4d131968b858 100644 (file)
--- a/helm/fix_params/cicFindParameters.ml
+++ b/helm/fix_params/cicFindParameters.ml
@@ -64,6 +64,7 @@ let rec parameters_of te ty pparams=
      | C.Cast (te, ty) -> aux te @@ aux ty
      | C.Prod (_, s, t) -> aux s @@ aux t
      | C.Lambda (_, s, t) -> aux s @@ aux t
+     | C.LetIn (_, s, t) -> aux s @@ aux t
      | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
      | C.Const (uri,_) ->
         (* the parameters could be not exact but only possible *)
@@ -85,7 +86,6 @@ let rec parameters_of te ty pparams=
           | C.CurrentProof _ -> S.empty (*CSC wrong *)
           | _ -> raise WrongUriToConstant
         )
-     | C.Abst _ -> S.empty
      | C.MutInd (uri,_,_) ->
         (match CicCache.get_obj uri with
             C.InductiveDefinition (_, params, _) ->
@@ -146,12 +146,12 @@ and fix_params uri filename =
  let module C = Cic in
   let ann = CicCache.get_annobj uri in
    match ann with
-      C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) ->
+      C.ADefinition (xid, id, te, ty, C.Possible pparams) ->
        let te' = Deannotate.deannotate_term te in
        let ty' = Deannotate.deannotate_term ty in
         let real_params = parameters_of te' ty' pparams in
          let fixed =
-          C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
+          C.ADefinition (xid,id,te,ty,C.Actual real_params)
          in
           Xml.pp (Cic2Xml.pp fixed uri) filename ;
     | _ -> ()