An unimplemented case of clearbody is now implemented.

[helm.git] / helm / software / components / tactics / proofEngineStructuralRules.ml

diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml
index ea7586e164f77c3a03079bdc9142481eb396ac70..755fab66051ee59197b081e85c3bdba20fdf04aa 100644 (file)
--- 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 _,_ =