Temporary (and partially broken) patch for Ferruccio: I duplicate

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 06a753f88d42f4b2e4475f06883b56e86e4ee08e..93cff174c4fb26e1c99334a761aef12e1b7aba14 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -76,15 +76,14 @@ let mk_rec_corec ng ind_kind defs loc =
     `MutualDefinition to rememer this. *)
   let name,ty = 
     match defs with
-    | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
+    | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+        let ty = match ty with Some ty -> ty | None -> N.Implicit in
         let ty =
          List.fold_right
           (fun var ty -> N.Binder (`Pi,var,ty)
           ) params ty
         in
          name,ty
-    | (_,(N.Ident (name, None), None),_,_) :: _ ->
-        name, N.Implicit
     | _ -> assert false 
   in
   let body = N.Ident (name,None) in