universal quantifier added

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

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 17378ffe79c8efffe0feaec4538f6871d2d1673e..2c641fd84f9ee3e48d625951bc970d35a61ed4e2 100644 (file)
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -67,10 +67,10 @@ let clearbody ~hyp =
                        _ ->
                          raise
                           (Fail
-                            ("The correctness of hypothesis " ^
+                            (lazy ("The correctness of hypothesis " ^
                              string_of_name n ^
                              " relies on the body of " ^ hyp)
-                          )
+                          ))
                      in
                       entry::context
                   | Some (_,Cic.Def (_,Some _)) -> assert false
@@ -84,8 +84,8 @@ let clearbody ~hyp =
                 _ ->
                  raise
                   (Fail
-                   ("The correctness of the goal relies on the body of " ^
-                    hyp))
+                   (lazy ("The correctness of the goal relies on the body of " ^
+                    hyp)))
               in
                m,canonical_context',ty
          | t -> t
@@ -111,34 +111,40 @@ let clear ~hyp =
       List.map
        (function
            (m,canonical_context,ty) when m = metano ->
-             let canonical_context' =
+             let context_changed, canonical_context' =
               List.fold_right
-               (fun entry context ->
+               (fun entry (b, context) ->
                  match entry with
-                    Some (Cic.Name hyp',_) when hyp' = hyp -> None::context
-                  | None -> None::context
+                    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,C.Def (t,None)) ->
-                     let _,_ =
-                      try
-                       CicTypeChecker.type_of_aux' metasenv context t
-                        CicUniv.empty_ugraph (* TASSI: FIXME *)
-                      with _ ->
-                       raise
-                        (Fail
-                          ("Hypothesis " ^ string_of_name n ^
-                           " uses hypothesis " ^ hyp))
-                     in
-                      entry::context
-               ) canonical_context []
+                      if b then
+                         let _,_ =
+                          try
+                           CicTypeChecker.type_of_aux' metasenv context t
+                            CicUniv.empty_ugraph
+                          with _ ->
+                           raise
+                            (Fail
+                              (lazy ("Hypothesis " ^ string_of_name n ^
+                               " uses hypothesis " ^ hyp)))
+                         in
+                          (b, entry::context)
+                      else
+                        (b, entry::context)
+               ) canonical_context (false, [])
              in
-              let _,_ =
+             if not context_changed then
+               raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
+             let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                 CicUniv.empty_ugraph (* TASSI: FIXME *)
+                 CicUniv.empty_ugraph 
                with _ ->
-                raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal"))
+                raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
               in
                m,canonical_context',ty
          | t -> t
@@ -155,4 +161,4 @@ let set_goal n =
        if CicUtil.exists_meta n metasenv then
          (proof, [n])
        else
-         raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))
+         raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))