X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineStructuralRules.ml;h=3f96677b8b01d8bd0e7c5bc07d419b26ccfccd3a;hb=d120acefa62d997341a84ec54cb1532e223dd661;hp=755fab66051ee59197b081e85c3bdba20fdf04aa;hpb=10d3194c1b42dfa72e51000ff2cc217f937b43ac;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml
index 755fab660..3f96677b8 100644
--- a/helm/software/components/tactics/proofEngineStructuralRules.ml
+++ b/helm/software/components/tactics/proofEngineStructuralRules.ml
@@ -46,21 +46,10 @@ let clearbody ~hyp =
                (fun entry context ->
                  match entry with
                     Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
-                     let cleared_entry =
-                      let ty =
-                       match ty with
-                          Some ty -> ty
-                        | None ->
-                           fst
-                            (CicTypeChecker.type_of_aux' metasenv context term
-                              CicUniv.empty_ugraph) (* TASSI: FIXME *)
-                      in
-                       Some (C.Name hyp, Cic.Decl ty)
-                     in
+                     let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in
                       cleared_entry::context
                   | None -> None::context
-                  | Some (n,C.Decl t)
-                  | Some (n,C.Def (t,None)) ->
+                  | Some (n,C.Decl t) ->
                      let _,_ =
                       try
                        CicTypeChecker.type_of_aux' metasenv context t
@@ -75,7 +64,7 @@ let clearbody ~hyp =
                           ))
                      in
                       entry::context
-                  | Some (n,Cic.Def (te,Some ty)) ->
+                  | Some (n,Cic.Def (te,ty)) ->
                      (try
                        ignore
                         (CicTypeChecker.type_of_aux' metasenv context te
@@ -136,8 +125,7 @@ let clear_one ~hyp =
                       (true, None::context)
                   | None -> (b, None::context)
                   | Some (n,C.Decl t)
-                  | Some (n,Cic.Def (t,Some _))
-                  | Some (n,C.Def (t,None)) ->
+                  | Some (n,Cic.Def (t,_)) ->
                       if b then
                          let _,_ =
                           try