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

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

diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml
index d9f0ce9a48f25e8eb9737ef51548b765dca72b30..8e443447a892f2a160fd7c724697698857a987b8 100644 (file)
--- a/components/tactics/fourierR.ml
+++ b/components/tactics/fourierR.ml
@@ -577,7 +577,7 @@ let tac_zero_inf_pos (n,d) =
    (*let cste = pf_parse_constr gl in*)
    let pall str (proof,goal) t =
      debug ("tac "^str^" :\n" );
-     let curi,metasenv,pbo,pty, attrs = proof in
+     let curi,metasenv,_subst,pbo,pty, attrs = proof in
      let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      debug ("th = "^ CicPp.ppterm t ^"\n"); 
      debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -675,7 +675,7 @@ let tac_zero_inf_false gl (n,d) =
 let tac_zero_infeq_false gl (n,d) =
  let tac_zero_infeq_false gl (n,d) status =
   let (proof, goal) = status in
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   
   debug("faccio fold di " ^ CicPp.ppterm
@@ -713,13 +713,13 @@ let tac_zero_infeq_false gl (n,d) =
 
 let apply_type_tac ~cast:t ~applist:al = 
  let apply_type_tac ~cast:t ~applist:al (proof,goal) = 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,t)::metasenv in
-   let proof' = curi,metasenv',pbo,pty, attrs in
+   let proof' = curi,metasenv',_subst,pbo,pty, attrs in
     let proof'',goals =
      apply_tactic 
       (PrimitiveTactics.apply_tac 
@@ -734,13 +734,13 @@ let apply_type_tac ~cast:t ~applist:al =
 
 let my_cut ~term:c =
  let my_cut ~term:c (proof,goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,c)::metasenv in
-   let proof' = curi,metasenv',pbo,pty, attrs in
+   let proof' = curi,metasenv',_subst,pbo,pty, attrs in
     let proof'',goals =
      apply_tactic 
       (apply_type_tac 
@@ -762,7 +762,7 @@ let tac_use h =
  let tac_use h status = 
   let (proof, goal) = status in
   debug("Inizio TC_USE\n");
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
   debug ("ty = "^ CicPp.ppterm ty^"\n");
@@ -873,7 +873,7 @@ let equality_replace a b =
  debug("inizio EQ\n");
   let module C = Cic in
    let proof,goal = status in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -886,7 +886,7 @@ let equality_replace a b =
        ~direction:`LeftToRight
        ~pattern:(ProofEngineTypes.conclusion_pattern None)
        (C.Meta (fresh_meta,irl)) [])
-     ((curi,metasenv',pbo,pty, attrs),goal)
+     ((curi,metasenv',_subst,pbo,pty, attrs),goal)
     in
     let new_goals = fresh_meta::goals in
  debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
@@ -934,7 +934,7 @@ let contradiction_tac (proof,goal)=
 (* ********************* TATTICA ******************************** *)
 
 let rec fourier (s_proof,s_goal)=
-  let s_curi,s_metasenv,s_pbo,s_pty, attrs = s_proof in
+  let s_curi,s_metasenv,_subst,s_pbo,s_pty, attrs = s_proof in
   let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
   debug_pcontext s_context;
@@ -974,7 +974,7 @@ let rec fourier (s_proof,s_goal)=
 
    (* now we have all the right environment *)
    
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
    (* now we want to convert hp to inequations, but first we must lift
@@ -1061,7 +1061,7 @@ let rec fourier (s_proof,s_goal)=
            (Tacticals.thens 
              ~start:(mk_tactic (fun status -> 
               debug ("inizio t1 strict\n");
-              let curi,metasenv,pbo,pty, attrs = proof in
+              let curi,metasenv,_subst,pbo,pty, attrs = proof in
               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
               debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -1092,7 +1092,7 @@ let rec fourier (s_proof,s_goal)=
              tac1:=(Tacticals.thens 
               ~start:(mk_tactic (fun status -> 
                 debug("INIZIO TAC 1 2\n");
-                let curi,metasenv,pbo,pty, attrs = proof in
+                let curi,metasenv,_subst,pbo,pty, attrs = proof in
                 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
                 debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -1128,7 +1128,7 @@ let rec fourier (s_proof,s_goal)=
          ~continuations:[Tacticals.then_  
            ~start:( mk_tactic (fun status ->
              let (proof, goal) = status in
-             let curi,metasenv,pbo,pty, attrs = proof in
+             let curi,metasenv,_subst,pbo,pty, attrs = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              apply_tactic 
               (ReductionTactics.change_tac
@@ -1167,7 +1167,7 @@ let rec fourier (s_proof,s_goal)=
                 Tacticals.then_ 
                  ~start:(mk_tactic (fun status ->
                    let (proof, goal) = status in
-                   let curi,metasenv,pbo,pty, attrs = proof in
+                   let curi,metasenv,_subst,pbo,pty, attrs = proof in
                    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                    (* check if ty is of type *)
                    let w1 =