]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/eliminationTactics.ml
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / tactics / eliminationTactics.ml
index 0aa33c2db5dd2082e5557b9212cb30cc2c51c380..bb269411ede2ec4749dba9a456d8dbc020a7fc56 100644 (file)
@@ -97,7 +97,7 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what =
                           ~continuation:(S.clear what)
         in
         E.apply_tactic tac status
-      else raise (E.Fail "unexported elim_clear: not an eliminable type") 
+      else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
    in
    E.mk_tactic elim_clear_tac