X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=8031e7bbd26b77c027c43fcd3a5e438813010770;hb=c39567bfa25333be8a51c969dabbaf0aeb4dfa57;hp=b16b133bac997364592db469ef3f8df0d77bd3cd;hpb=fc4cf455977934bd737c3d6c8675ef7663a6a588;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index b16b133ba..8031e7bbd 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -145,7 +145,7 @@ let build_inversion uri obj =
  if List.length (list_of_prod arity) = (nleft + 1) then
   None
  else
-  begin
+  try
    let arity_l = cut_last (list_of_prod arity) in
    let rightparam_tys = cut_first nleft arity_l in
    let theorem = build_theorem rightparam_tys arity_l arity cons_list 
@@ -194,7 +194,8 @@ let build_inversion uri obj =
    Some
     (inversor_uri,
     Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
-  end
+  with
+   Inversion.EqualityNotDefinedYet -> None
 ;;
 
 let init () = ();;