new pp function for proofs

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

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index 0ff369a9a6d4b4367cfeec9bce090c386eeeb029..f5e2a847690f2b4c20544c32d9a18ba25108177c 100644 (file)
--- 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