]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2content.ml
* added new .ml files to be ignored
[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml
index 2c46c3c46a23238d818740a18c2aec39642a7d96..614848706f5110a6398937d9548a5d305038c8cc 100644 (file)
@@ -754,7 +754,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                 K.conclude_method = method_name;
                 K.conclude_args =
                   K.Aux (string_of_int no_constructors) 
-                  ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
+                  ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
                   ::method_args@other_method_args;
                 K.conclude_conclusion = 
                    try Some