minimal changes:

[helm.git] / helm / ocaml / cic / deannotate.ml

diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml
index c27a9d576bc225c4f15b8eca40b6d9d8a1dc142f..df59305fea29d1af45a52dc3f771234775e94448 100644 (file)
--- a/helm/ocaml/cic/deannotate.ml
+++ b/helm/ocaml/cic/deannotate.ml
@@ -82,7 +82,7 @@ and deannotate_coinductiveFun (_,name,ty,bo) =
  (name, deannotate_term ty, deannotate_term bo)
 ;;
 
-let deannotate_inductiveType (name, isinductive, arity, cons) =
+let deannotate_inductiveType (_, name, isinductive, arity, cons) =
  (name, isinductive, deannotate_term arity,
   List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
 ;;
@@ -119,6 +119,6 @@ let deannotate_obj =
        deannotate_term bo,deannotate_term ty,params
       )
    | C.AInductiveDefinition (_, tys, params, parno) ->
-      C.InductiveDefinition ( List.map deannotate_inductiveType tys,
+      C.InductiveDefinition (List.map deannotate_inductiveType tys,
        params, parno)
 ;;