From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2008 11:06:26 +0000 (+0000)
Subject: An unimplemented case of clearbody is now implemented.
X-Git-Tag: make_still_working~5545
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10d3194c1b42dfa72e51000ff2cc217f937b43ac;p=helm.git

An unimplemented case of clearbody is now implemented.
---

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 _,_ =