inductive type ident optional in mutcase

[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index fc6d9553174fbf2521dba05ed7228fe1a79db07b..19b6c4b4bf4161ab4546d2f178fe9e13d2c117be 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -166,7 +166,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
               ((name, capture_variables), rhs))
             constructors patterns
         in
-        idref id (Ast.Case (aux te, name, Some (aux ty), patterns))
+        idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map