X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Finversion_principle.ml;h=45ece4823a95caf0d54d9cf578841830f1962c40;hb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;hp=b0f4d236ff5aa23e3fefad53b73e831c578e3274;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git

diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index b0f4d236f..45ece4823 100644
--- a/components/tactics/inversion_principle.ml
+++ b/components/tactics/inversion_principle.ml
@@ -154,8 +154,9 @@ let build_inversion uri obj =
 	     let goal = CicMkImplicit.new_meta metasenv [] in
 	     let metasenv' = (goal,[],ref_theorem)::metasenv in
 	     let attrs = [`Class (`InversionPrinciple); `Generated] in
+       let _subst = [] in
 	     let proof= 
-	       (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in 
+	       (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in 
 	     let _,applies =
 	       List.fold_right
 		 (fun _ (i,applies) ->
@@ -186,7 +187,7 @@ let build_inversion uri obj =
 		 (proof,goal) 
 	     in
 	     let metasenv,bo,ty, attrs =
-	       match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
+	       match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
 	     in
 	       assert (metasenv = []);
 	       Some