parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml
index 4d4f305ae5684d134df97b137e3e7f90afb66c07..eb3201c58587b051170991690254d29a17434148 100644 (file)
--- a/helm/software/components/tactics/fourierR.ml
+++ b/helm/software/components/tactics/fourierR.ml
@@ -439,8 +439,8 @@ let fourier_lineq lineq1 =
    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
                Hashtbl.iter (fun x c ->
-                                 try (Hashtbl.find hvar x;())
-                                 with _-> nvar:=(!nvar)+1;
+                                 try ignore(Hashtbl.find hvar x)
+                                 with Not_found -> nvar:=(!nvar)+1;
                                              Hashtbl.add hvar x (!nvar);
                                           debug("aggiungo una var "^
                                            string_of_int !nvar^" per "^
@@ -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");
@@ -858,11 +858,9 @@ let rec superlift c n=
     [] -> []
   | Some(name,Cic.Decl(a))::next  -> 
      [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1)
-  | Some(name,Cic.Def(a,None))::next -> 
-     [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1)
-  | Some(name,Cic.Def(a,Some ty))::next   -> 
+  | Some(name,Cic.Def(a,ty))::next   -> 
      [Some(name,
-      Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
+      Cic.Def((CicSubstitution.lift n a),CicSubstitution.lift n ty))
       ] @ superlift next (n+1)
   | _::next -> superlift next (n+1) (*??  ??*)
  
@@ -873,7 +871,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 +884,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 +932,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 +972,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 +1059,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 +1090,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 +1126,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
@@ -1161,13 +1159,13 @@ let rec fourier (s_proof,s_goal)=
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
                    Tacticals.first 
-                     ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
+                     ~tactics:[Ring.ring_tac; Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)
                 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 =