X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=15d7968d34c5476e5192fa4c085c4d544bccc59f;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=9e91eeb07fad9f5f58a20bd3b94c873660397cff;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 9e91eeb07..15d7968d3 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -31,7 +31,7 @@ let rec injection_tac ~term ~status:((proof, goal) as status) =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in  
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
@@ -83,7 +83,7 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
@@ -151,7 +151,7 @@ prerr_endline ("XXXX cominciamo!") ;
                     ~start:
                       (fun ~status:((proof,goal) as status) ->    
                         let _,metasenv,_,_ = proof in
-                         let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+                         let _,context,gty = CicUtil.lookup_meta goal metasenv in
 prerr_endline ("XXXX goal " ^ string_of_int goal) ;
 prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
 prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
@@ -207,7 +207,7 @@ let discriminate'_tac ~term ~status:((proof, goal) as status) =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
@@ -291,21 +291,9 @@ prerr_endline ("XXXX nth funzionano ") ;
                      (match goals' with
                          [goal'] -> 
                           let _,metasenv',_,_ = proof' in
-                           let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (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])) ;
+                           let _,context',gty' =
+                             CicUtil.lookup_meta goal' metasenv'
+                           in
                             T.then_
                              ~start:
                               (P.change_tac 
@@ -375,7 +363,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,gty = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with
          (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
@@ -431,7 +419,7 @@ let discriminate_tac ~term ~status:((proof, goal) as status) =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
@@ -516,21 +504,9 @@ prerr_endline ("XXXX nth funzionano ") ;
                      (match goals' with
                          [goal'] -> 
                           let _,metasenv',_,_ = proof' in
-                           let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (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'])) ;
+                           let _,context',gty' =
+                             CicUtil.lookup_meta goal' metasenv'
+                           in
                             T.then_
                              ~start:
                               (P.change_tac