1. new syntax for patterns:

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 24ab511f05d71c77f08e83e186b8be41f67f27d2..05344e0abf93d9debb2135047c297a6528d3dbab 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -164,23 +164,21 @@ and injection1_tac ~term ~i =
                            in
                             ProofEngineTypes.apply_tactic 
                             (P.change_tac
-                               ~what:new_t1'
-                               ~pattern:([],None)
-                               ~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]
-                                 ))
+                               ~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:
@@ -300,20 +298,18 @@ let discriminate'_tac ~term =
                             (T.then_
                              ~start:
                               (P.change_tac 
-                               ~what:gty' 
-                               ~pattern:([],None)
-                               ~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]
-                                )
+                               ~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:
                               (