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 e1bedeb207ff473653f1a06899b14df780b96c0d..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.empty_ugraph
+    ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
       ~conjecture ~pattern
   in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
@@ -67,17 +67,9 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
           Some (name,Cic.Decl ty')::context', metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
           let bo', metasenv, ugraph =
-            change subst bo selected_bo metasenv ugraph
-          in
+            change subst bo selected_bo metasenv ugraph in
           let ty', metasenv, ugraph =
-           match ty,selected_ty with
-              None,None -> None, metasenv, ugraph
-            | Some ty,Some selected_ty ->
-                let ty', metasenv, ugraph =
-                  change subst ty selected_ty metasenv ugraph
-                in
-                Some ty', metasenv, ugraph
-            | _,_ -> assert false
+            change subst ty selected_ty metasenv ugraph
           in
            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
@@ -88,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 =
@@ -143,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
@@ -155,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
@@ -175,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.empty_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
@@ -190,17 +185,9 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
            (Some (name,Cic.Decl ty')::context'), metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
           let bo', metasenv, ugraph =
-            change subst bo selected_bo metasenv ugraph
-          in
+            change subst bo selected_bo metasenv ugraph in
           let ty', metasenv, ugraph =
-           match ty,selected_ty with
-              None,None -> None, metasenv, ugraph
-            | Some ty,Some selected_ty ->
-                let ty', metasenv, ugraph =
-                  change subst ty selected_ty metasenv ugraph
-                in
-                Some ty', metasenv, ugraph
-            | _,_ -> assert false
+            change subst ty selected_ty metasenv ugraph
           in
            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
@@ -212,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,_) =
@@ -227,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 =
@@ -241,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)
+;;