removed dependency on netclient, use http_client module from ocaml-http

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 16be77edb443c84c3c7845182564dacfb1601cce..79304211deb0e8a69f3f1072a8657dc2a33510fa 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -36,6 +36,7 @@ let mk_fresh_name context name ~typ =
        (try
          (match CicTypeChecker.type_of_aux' [] context typ with
              C.Sort C.Prop -> "H"
+          | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"
            | _ -> "H"
          )
@@ -100,8 +101,9 @@ let subst_meta_in_proof proof meta term newmetasenv =
          List.map
           (function
               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
             | None -> None
+            | Some (_,Cic.Def (_,Some _)) -> assert false
           ) canonical_context
         in
          i,canonical_context',(subst_in ty)
@@ -136,7 +138,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
              (function
                  None -> None
                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
-               | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
+               | Some (i,Cic.Def (t,None))  ->
+                  Some (i,Cic.Def ((subst_in t),None))
+               | Some (_,Cic.Def (_,Some _))  -> assert false
              ) canonical_context
            in
             (m,canonical_context',subst_in ty)::i