From 10d3194c1b42dfa72e51000ff2cc217f937b43ac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 11:06:26 +0000 Subject: [PATCH] An unimplemented case of clearbody is now implemented. --- .../tactics/proofEngineStructuralRules.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index ea7586e16..755fab660 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -75,7 +75,23 @@ let clearbody ~hyp = )) in entry::context - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (te,Some ty)) -> + (try + ignore + (CicTypeChecker.type_of_aux' metasenv context te + CicUniv.empty_ugraph (* TASSI: FIXME *)); + ignore + (CicTypeChecker.type_of_aux' metasenv context ty + CicUniv.empty_ugraph (* TASSI: FIXME *)); + with + _ -> + raise + (PET.Fail + (lazy ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ hyp) + ))); + entry::context ) canonical_context [] in let _,_ = -- 2.39.2