X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=ccac132ef6b631b46504d9e63b96c1af5ed8804c;hb=bafecec2d4af08af32249b4ec75db477a6024c7b;hp=16be77edb443c84c3c7845182564dacfb1601cce;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 16be77edb..ccac132ef 100644
--- 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"
          )
@@ -60,36 +61,12 @@ let mk_fresh_name context name ~typ =
       try_next 1
 ;;
 
-(* identity_relocation_list_for_metavariable i canonical_context         *)
-(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
-(* where n = List.length [canonical_context]                             *)
-(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
- let canonical_context_length = List.length canonical_context in
-  let rec aux =
-   function
-      (_,[]) -> []
-    | (n,None::tl) -> None::(aux ((n+1),tl))
-    | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
-  in
-   aux (1,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta.                       *)
-let new_meta ~proof =
- let (_,metasenv,_,_) = proof in
-  let rec aux =
-   function
-      None,[] -> 1
-    | Some n,[] -> n
-    | None,(n,_,_)::tl -> aux (Some n,tl)
-    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
-  in
-   1 + aux (None,metasenv)
+let new_meta_of_proof ~proof:(_, metasenv, _, _) =
+  CicMkImplicit.new_meta metasenv
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,bo,ty = proof in
-  let subst_in = CicUnification.apply_subst [meta,term] in
+  let subst_in = CicMetaSubst.apply_subst [meta,term] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
    in
@@ -100,8 +77,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 +114,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