CSC: tentative definition of the ocaml structure that represents

[helm.git] / helm / gTopLevel / content2cic.ml

diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml
index 17ba99ed8193797919c52f6981b2935b837670e6..a4f8cd1ae4a0c99b04dd08662acd9c1529756797 100644 (file)
--- 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 =