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

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

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index 2cfd95e9a96ed0cc71392f2bb36e64e42d68ee3e..6b87de349ce7f2225b54835e968b6cb54c7d6463 100644 (file)
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -109,7 +109,7 @@ let filter_uris_backward ~dbd ~facts signature uris =
     intersect uris siguris 
 
 let compare_goal_list proof goal1 goal2 =
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv, _subst, _,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = 
@@ -195,7 +195,7 @@ let cmatch' = Constr.cmatch'
 
 (* used only by te old auto *)
 let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
  let set = signature_of_hypothesis context metasenv in
@@ -344,7 +344,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
     ^ "\n}"
   in
 *)
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
    match signature with 
@@ -394,7 +394,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
 
 let experimental_hint 
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
-  let (_, metasenv, _, _, _) = proof in
+  let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
@@ -478,7 +478,7 @@ let new_experimental_hint
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
-  let (_, metasenv, _, _, _) = proof in
+  let (_, metasenv,  _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with