many changes:

[helm.git] / helm / software / components / acic_content / content2cic.ml

diff --git a/helm/software/components/acic_content/content2cic.ml b/helm/software/components/acic_content/content2cic.ml
index 9acea81fa903b8455c830763b5a4c26fef365b66..dcec61d84a478018a003a1623227ed8249b79dac 100644 (file)
--- a/helm/software/components/acic_content/content2cic.ml
+++ b/helm/software/components/acic_content/content2cic.ml
@@ -141,7 +141,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "2"; assert false)
     else if conclude.Con.conclude_method = "Exact" then
       (match conclude.Con.conclude_args with
-         [Con.Term t] -> deannotate t
+         [Con.Term (_,t)] -> deannotate t
        | [Con.Premise prem] -> 
            (match prem.Con.premise_n with
               None -> assert false
@@ -156,7 +156,7 @@ 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 (
+         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 
@@ -166,7 +166,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "5"; assert false)
     else if (conclude.Con.conclude_method = "Rewrite") then
       (match conclude.Con.conclude_args with
-         Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
+         Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args ->
            let subst =
              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
            let  cargs = args2cic premise_env args in
@@ -174,7 +174,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "6"; assert false)
     else if (conclude.Con.conclude_method = "Case") then
       (match conclude.Con.conclude_args with
-        Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+        Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Premise(prem)::patterns ->
            C.MutCase
             (UriManager.uri_of_string uri,
              int_of_string notype, deannotate ty, 
@@ -183,7 +183,7 @@ let proof2cic deannotate p =
                (function 
                    Con.ArgProof p -> proof2cic [] p
                  | _ -> prerr_endline "7a"; assert false) patterns)
-      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
+      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Term(_,te)::patterns ->           C.MutCase
             (UriManager.uri_of_string uri,
              int_of_string notype, deannotate ty, deannotate te,
              List.map 
@@ -214,7 +214,7 @@ let proof2cic deannotate p =
                   raise Not_found))
       | Con.Lemma lemma ->
          CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
-      | Con.Term t -> deannotate t
+      | Con.Term (_,t) -> deannotate t
       | Con.ArgProof p -> proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO