X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=b16b133bac997364592db469ef3f8df0d77bd3cd;hb=1589ec067f5f18594dfcab61431adbe095db1bd1;hp=2138893d3b5ab7d163e33f87f9df7fc0b71e714c;hpb=d8f4d935054a6f9fff6de0c171dc4a181389219e;p=helm.git diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index 2138893d3..b16b133ba 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/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 *)