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

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 2e8aa4049..8995fbbeb 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -118,8 +118,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 _,_ =