X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=2cc72933b884cbaca2eeea3ddc2b1d51ed625db3;hb=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;hp=65ea0d3069efc56f460ac632aefaf4590732531a;hpb=e1d3db51fb0d63c882c0a40d9b91bc28ab05747e;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 65ea0d306..2cc72933b 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -154,8 +154,8 @@ let proof2cic deannotate p =
              conclude.Con.conclude_method = "Exists" ||
              conclude.Con.conclude_method = "FalseInd") then
       (match (List.tl conclude.Con.conclude_args) with
-         Con.Term (C.AAppl 
-            id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
+         Con.Term (C.AAppl (
+            id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
            let subst =
              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in 
            let cargs = args2cic premise_env args in