]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/fix_params/cicFindParameters.ml
...
[helm.git] / helm / fix_params / cicFindParameters.ml
index 555f44e2e482ae2b0d4c67d20fdb55344b84900d..f746751553d4970950f111e476864cde0bcc248c 100644 (file)
@@ -147,12 +147,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 ;
     | _ -> ()