X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=4677a33ac8221a1080d7d0f6953e9fe2b8a822ba;hb=6bbeb650abc3a94e76d683aa47b2e46254d495d1;hp=2e8aa404930f54a58f85810cd165ddaabc767c04;hpb=252fbb53c9d41d5d3f94bd9656adde26cd603ae3;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 2e8aa4049..4677a33ac 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open ProofEngineTypes
 
 let clearbody ~hyp = 
@@ -118,8 +120,8 @@ let clear ~hyp =
                     Some (Cic.Name hyp',_) when hyp' = hyp -> 
                       (true, None::context)
                   | None -> (b, None::context)
-                  | Some (_,Cic.Def (_,Some _)) -> assert false
                   | Some (n,C.Decl t)
+                  | Some (n,Cic.Def (t,Some _))
                   | Some (n,C.Def (t,None)) ->
                       if b then
                          let _,_ =