parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index c943e7a19cafdf592426615182dfdd5cdd4bdf07..2684222d4e37f1072e834e69978c6ebd8708f148 100644 (file)
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -30,7 +30,7 @@ open ProofEngineTypes
 (* Note: this code is almost identical to change_tac and
 *  it could be unified by making the change function a callback *)
 let reduction_tac ~reduction ~pattern (proof,goal) =
-  let curi,metasenv,_subst,pbo,pty, attrs = proof in
+  let curi,metasenv,subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
      CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
+    ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
       ~conjecture ~pattern
   in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
@@ -80,7 +80,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
       | _ as t -> t
     ) metasenv
   in
-  (curi,metasenv',_subst,pbo,pty, attrs), [metano]
+  (curi,metasenv',subst,pbo,pty, attrs), [metano]
 ;;
 
 let simpl_tac ~pattern =
@@ -135,7 +135,7 @@ exception NotConvertible
         term(s) to be replaced. *)
 let change_tac ?(with_cast=false) ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
-  let curi,metasenv,_subst,pbo,pty, attrs = proof in
+  let curi,metasenv,subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -147,10 +147,12 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
             with_what context_of_t metasenv ugraph
           in
           let _,u =
-            CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
+            CicTypeChecker.type_of_aux' 
+              metasenv ~subst context_of_t with_what ugraph
           in
           let b,_ =
-           CicReduction.are_convertible ~metasenv context_of_t t with_what u
+           CicReduction.are_convertible 
+             ~metasenv ~subst context_of_t t with_what u
           in
           if b then
            ((t, with_what) :: pairs), metasenv, ugraph
@@ -167,8 +169,9 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
       CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
-    ~pattern in
+   ProofEngineHelpers.select 
+     ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern 
+  in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
   let context', metasenv, ugraph =
    List.fold_right2
@@ -196,7 +199,7 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
         | _ as t -> t)
       metasenv
   in
-   let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+   let proof,goal = (curi,metasenv',subst,pbo,pty, attrs), metano in
     if with_cast then
      let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (newproof,_) =
@@ -211,6 +214,7 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
      proof,[goal]
   in
     mk_tactic (change_tac ~pattern ~with_what)
+;;
 
 let fold_tac ~reduction ~term ~pattern =
  let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
@@ -225,4 +229,5 @@ let fold_tac ~reduction ~term ~pattern =
     (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
  in
   mk_tactic (fold_tac ~reduction ~term ~pattern)
+;;