From 87708967ed20000d7fb10ed04596a0c0c0ffafe1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Nov 2005 17:58:17 +0000 Subject: [PATCH] Invariant no longer true (since when?) --- helm/ocaml/tactics/proofEngineStructuralRules.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 _,_ = -- 2.39.2