X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Finversion.ml;h=f5e2a847690f2b4c20544c32d9a18ba25108177c;hb=f6edef464aae7bbf001f77dcaf256f67960d0e47;hp=0ff369a9a6d4b4367cfeec9bce090c386eeeb029;hpb=7803bba7862a492252d520d670614738b866ae1e;p=helm.git

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index 0ff369a9a..f5e2a8476 100644
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -209,8 +209,7 @@ let private_inversion_tac ~term =
   (List.map 
    (fun t -> (
     match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
-     (term,graph) -> term
-     |_ -> assert false))
+     (term,graph) -> term))
    parameters) 
  in
  let consno = List.length cons_list in