X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcontent2cic.ml;h=a4f8cd1ae4a0c99b04dd08662acd9c1529756797;hb=4a01e6197e070d3eff7a3fe02180597136d81eba;hp=17ba99ed8193797919c52f6981b2935b837670e6;hpb=62820aacb94856be5cd2e125032669245ca1408d;p=helm.git

diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml
index 17ba99ed8..a4f8cd1ae 100644
--- a/helm/gTopLevel/content2cic.ml
+++ b/helm/gTopLevel/content2cic.ml
@@ -55,31 +55,31 @@ let proof2cic term2cic p =
     let module C = Cic in
     let module Con = Cic2content in
       match ce with
-        Con.Declaration d -> 
+        `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
                 C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
             | None -> 
                 C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
-      | Con.Hypothesis h ->
+      | `Hypothesis h ->
           (match h.Con.dec_name with
               Some s ->
                 C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
             | None -> 
                 C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
-      | Con.Proof p -> 
+      | `Proof p -> 
           (match p.Con.proof_name with
               Some s ->
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | Con.Definition d -> 
+      | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | Con.Joint ho -> 
+      | `Joint ho -> 
             raise TO_DO 
 
   and conclude2cic premise_env conclude =