changed default parameter values...

[helm.git] / helm / ocaml / tactics / discriminationTactics.ml

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 96822d8e85af0511a90d1413a4632dfbbab522c7..590b482c716db80b74b83429aa4808fbb804aa38 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-open HelmLibraryObjects
-
 let debug_print = fun _ -> ()
 
 let rec injection_tac ~term =
@@ -41,7 +39,7 @@ let rec injection_tac ~term =
     ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -97,7 +95,7 @@ and injection1_tac ~term ~i =
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with (* some inductive type *)
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -163,28 +161,31 @@ and injection1_tac ~term ~i =
                              | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
                            in
                             ProofEngineTypes.apply_tactic 
-                            (P.change_tac
-                               ~what:new_t1'
-                               ~with_what:
-                                 (C.Appl [
-                                   C.Lambda (
-                                    C.Name "x", tty,
-                                    C.MutCase (
-                                     turi, typeno,
-                                     (C.Lambda (
-                                      (C.Name "x"),
-                                      (S.lift 1 tty),
-                                      (S.lift 2 tty'))),
-                                     (C.Rel 1), pattern
-                                    )
-                                   );
-                                   t1]
-                                 ))
+                            (ReductionTactics.change_tac
+                               ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
+                               (C.Appl [
+                                 C.Lambda (
+                                  C.Name "x", tty,
+                                  C.MutCase (
+                                   turi, typeno,
+                                   (C.Lambda (
+                                    (C.Name "x"),
+                                    (S.lift 1 tty),
+                                    (S.lift 2 tty'))),
+                                   (C.Rel 1), pattern
+                                  )
+                                 );
+                                 t1]
+                               ))
                         status
                        ))
                      ~continuation:
                        (T.then_
-                         ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+                         ~start:
+                           (EqualityTactics.rewrite_simpl_tac
+                             ~direction:`LeftToRight
+                             ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                             term)
                          ~continuation:EqualityTactics.reflexivity_tac
                        )
                    ])     
@@ -216,7 +217,7 @@ let discriminate'_tac ~term =
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
-          when (U.eq equri Logic.eq_URI) -> (
+          when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -275,8 +276,8 @@ let discriminate'_tac ~term =
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd(Logic.false_URI,0,[]))
-                                     else (C.MutInd(Logic.true_URI,0,[]))
+                                     then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+                                     else (C.MutInd(LibraryObjects.true_URI (),0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -286,7 +287,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
                     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(Logic.false_URI,0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with
@@ -298,25 +299,28 @@ let discriminate'_tac ~term =
                            ProofEngineTypes.apply_tactic
                             (T.then_
                              ~start:
-                              (P.change_tac 
-                               ~what:gty' 
-                               ~with_what:
-                                (C.Appl [
-                                  C.Lambda (
-                                   C.Name "x", tty, 
-                                   C.MutCase (
-                                    turi, typeno,
-                                    (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
-                                    (C.Rel 1), pattern
-                                   )
-                                  ); 
-                                  t2]
-                                )
+                              (ReductionTactics.change_tac 
+                               ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
+                               (C.Appl [
+                                 C.Lambda (
+                                  C.Name "x", tty, 
+                                  C.MutCase (
+                                   turi, typeno,
+                                   (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
+                                   (C.Rel 1), pattern
+                                  )
+                                 ); 
+                                 t2]
+                               )
                               )
                              ~continuation:
                               (
                                  T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
+                                   ~start:
+                                     (EqualityTactics.rewrite_simpl_tac
+                                       ~direction:`RightToLeft
+                                       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                                       term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               ))
                              (proof',goal')