X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=7f4a89fb868bb0da871403047dc7dc4cd922d3a7;hb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;hp=d89420f58cde8526c4d578341db8633db23c7f10;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index d89420f58..7f4a89fb8 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -29,10 +29,11 @@ let clearbody ~hyp ~status:(proof, goal) =
  let module C = Cic in
   match hyp with
      None -> assert false
+   | Some (_, C.Def (_, Some _)) -> assert false
    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
-   | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+   | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
       let curi,metasenv,pbo,pty = proof in
-       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+       let metano,_,_ = CicUtil.lookup_meta goal metasenv in
         let string_of_name =
          function
             C.Name n -> n
@@ -56,7 +57,7 @@ let clearbody ~hyp ~status:(proof, goal) =
                          cleared_entry::context
                      | None -> None::context
                      | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
+                     | Some (n,C.Def (t,None)) ->
                         let _ =
                          try
                           CicTypeChecker.type_of_aux' metasenv context t
@@ -71,6 +72,7 @@ let clearbody ~hyp ~status:(proof, goal) =
                              )
                         in
                          entry::context
+                     | Some (_,Cic.Def (_,Some _)) -> assert false
                   ) canonical_context []
                 in
                  let _ =
@@ -96,7 +98,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
    | Some (n_to_clear, _) ->
       let curi,metasenv,pbo,pty = proof in
        let metano,context,ty =
-        List.find (function (m,_,_) -> m=goal) metasenv
+        CicUtil.lookup_meta goal metasenv
        in
         let string_of_name =
          function
@@ -113,8 +115,9 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
                     match entry with
                        t when t == hyp_to_clear -> None::context
                      | None -> None::context
+                     | Some (_,Cic.Def (_,Some _)) -> assert false
                      | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
+                     | Some (n,C.Def (t,None)) ->
                         let _ =
                          try
                           CicTypeChecker.type_of_aux' metasenv context t