- new tactic subst removes simple non recursive equalities from the context

[helm.git] / components / tactics / inversion_principle.ml

diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index 2138893d3b5ab7d163e33f87f9df7fc0b71e714c..8031e7bbd26b77c027c43fcd3a5e438813010770 100644 (file)
--- a/components/tactics/inversion_principle.ml
+++ b/components/tactics/inversion_principle.ml
@@ -105,7 +105,6 @@ let rec get_prop_arity sort rightparam_tys(*only to name m's*) created_vars_ty
      Cic.Sort(Cic.Prop))
    else
     Cic.Sort Cic.Prop
-  | _ -> assert false
 ;;
 
 (* created vars is empty at the beginning *)
@@ -146,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 
@@ -195,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 () = ();;