added support for repository attributes

[helm.git] / helm / ocaml / tactics / proofEngineStructuralRules.ml

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 2e8aa404930f54a58f85810cd165ddaabc767c04..4677a33ac8221a1080d7d0f6953e9fe2b8a822ba 100644 (file)
--- 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 _,_ =