added a (for the moment) dummy field _subst to ProofengineTypes.proof.

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

diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index b0f4d236ff5aa23e3fefad53b73e831c578e3274..45ece4823a95caf0d54d9cf578841830f1962c40 100644 (file)
--- 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