s/List.find.../CicUtil.lookup_meta/

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 9e91eeb07fad9f5f58a20bd3b94c873660397cff..15d7968d34c5476e5192fa4c085c4d544bccc59f 100644 (file)
--- 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 

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index b6141094fc2c7cbd2cb8be8c2e2cf34131b1fe2f..cd401a2ec94cdaa66a0200c3bb516907b9ef3460 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -44,7 +44,7 @@ let induction_tac ~term ~status:((proof,goal) as status) =
   let module S = ProofEngineStructuralRules in
   let module U = UriManager in 
    let (_,metasenv,_,_) = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
 
      T.then_ ~start:(T.repeat_tactic 
@@ -137,7 +137,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
   let module T = Tacticals in
   let module S = ProofEngineStructuralRules in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let old_context_len = List.length context in
      let termty = CicTypeChecker.type_of_aux' metasenv context term in
 
@@ -178,7 +178,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
          warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
          if nr_of_hyp_still_to_elim <> 0 then
           let _,metasenv,_,_ = proof in
-           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+           let _,context,_ = CicUtil.lookup_meta goal metasenv in
             let old_context_len = List.length context in
             let termty = CicTypeChecker.type_of_aux' metasenv context term' in
              warn ("elim_clear termty= " ^ CicPp.ppterm termty);
@@ -193,7 +193,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
                         (* clear the hyp that has just been eliminated *)
                         (fun ~status:((proof,goal) as status) -> 
                           let _,metasenv,_,_ = proof in
-                           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+                           let _,context,_ = CicUtil.lookup_meta goal metasenv in
                             let new_context_len = List.length context in   
                              warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
                              let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 3af6b861dd4ddafc15c18b0e8aff8d43ecba6bc6..48d5ea9a63e705780a49784989a59148d852c0b6 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -28,7 +28,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
  let module C = Cic in
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
    let eq_ind_r,ty,t1,t2 =
     match CicTypeChecker.type_of_aux' metasenv context equality with
        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
@@ -89,7 +89,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
  let module C = Cic in
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
    let eq_ind_r,ty,t1,t2 =
     match CicTypeChecker.type_of_aux' metasenv context equality with
        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
@@ -154,7 +154,7 @@ let replace_tac ~what ~with_what ~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 wty = CicTypeChecker.type_of_aux' metasenv context what in
       try
       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
@@ -200,7 +200,7 @@ let symmetry_tac ~status:(proof, goal) =
   let module R = CicReduction in
   let module U = UriManager in
    let (_,metasenv,_,_) = proof in
-    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
          PrimitiveTactics.apply_tac ~status:(proof,goal)
@@ -220,7 +220,7 @@ let transitivity_tac ~term ~status:((proof, goal) as status) =
   let module U = UriManager in
   let module T = Tacticals in
    let (_,metasenv,_,_) = proof in
-    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
          T.thens

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 537ef3f5d986f06286ca7ea341cb9d2c750bed0f..eeda7a862a83ce2d9a6771ff5d3c7d6f57f14e07 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -597,7 +597,7 @@ let tac_zero_inf_pos (n,d) ~status =
    let pall str ~status:(proof,goal) t =
      debug ("tac "^str^" :\n" );
      let curi,metasenv,pbo,pty = proof in
-     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      debug ("th = "^ CicPp.ppterm t ^"\n"); 
      debug ("ty = "^ CicPp.ppterm ty^"\n"); 
    in
@@ -678,7 +678,7 @@ let tac_zero_inf_false gl (n,d) ~status=
      (debug "2\n";let r = (Tacticals.then_ ~start:(
        fun ~status:(proof,goal as status) -> 
        let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+       let metano,context,ty = CicUtil.lookup_meta goal metasenv in
          debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
          ^ CicPp.ppterm ty ^"\n");
        let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
@@ -698,7 +698,7 @@ let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
 debug("stat tac_zero_infeq_false\n");
 let r = 
      let curi,metasenv,pbo,pty = proof in
-     let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      
      debug("faccio fold di " ^ CicPp.ppterm
             (Cic.Appl
@@ -736,7 +736,7 @@ let r =
 
 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -757,7 +757,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
    
 let my_cut ~term:c ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
 debug("my_cut di "^CicPp.ppterm c^"\n");
 
@@ -784,7 +784,7 @@ let exact = PrimitiveTactics.exact_tac;;
 let tac_use h ~status:(proof,goal as status) = 
 debug("Inizio TC_USE\n");
 let curi,metasenv,pbo,pty = proof in
-let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
 debug ("ty = "^ CicPp.ppterm ty^"\n"); 
 
@@ -899,7 +899,7 @@ debug("inizio EQ\n");
  let module C = Cic in
   let proof,goal = status in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
    let irl =
@@ -925,7 +925,7 @@ let tcl_fail a ~status:(proof,goal) =
 (* Galla: moved in variousTactics.ml 
 let assumption_tac ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let num = ref 0 in
   let tac_list = List.map 
        ( fun x -> num := !num + 1;
@@ -955,9 +955,7 @@ let contradiction_tac ~status:(proof,goal)=
 
 let rec fourier ~status:(s_proof,s_goal)=
   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
-  let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) 
-   s_metasenv in
-       
+  let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
   debug_pcontext s_context;
 
@@ -998,7 +996,7 @@ theoreme,so let's parse our thesis *)
    (* now we have all the right environment *)
    
    let curi,metasenv,pbo,pty = proof in
-   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
 
    (* now we want to convert hp to inequations, but first we must lift
@@ -1087,8 +1085,7 @@ theoreme,so let's parse our thesis *)
              fun ~status -> 
              debug ("inizio t1 strict\n");
              let curi,metasenv,pbo,pty = proof in
-             let metano,context,ty = List.find 
-              (function (m,_,_) -> m=goal) metasenv in
+             let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
              debug ("ty = "^ CicPp.ppterm ty^"\n"); 
               PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
@@ -1124,8 +1121,7 @@ theoreme,so let's parse our thesis *)
                fun ~status -> 
                debug("INIZIO TAC 1 2\n");
                let curi,metasenv,pbo,pty = proof in
-               let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
-                metasenv in
+               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
                debug ("ty = "^ CicPp.ppterm ty^"\n"); 
                 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
@@ -1163,8 +1159,7 @@ theoreme,so let's parse our thesis *)
          ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_  
           ~start:(fun ~status:(proof,goal as status) ->
              let curi,metasenv,pbo,pty = proof in
-             let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
-             metasenv in
+             let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              PrimitiveTactics.change_tac ~what:ty 
              ~with_what:(Cic.Appl [ _not; ineq]) ~status)
           ~continuation:(Tacticals.then_ 
@@ -1203,8 +1198,7 @@ theoreme,so let's parse our thesis *)
                  (
                  fun ~status:(proof,goal as status) ->
                   let curi,metasenv,pbo,pty = proof in
-                  let metano,context,ty = List.find (function (m,_,_) -> m=
-                   goal) metasenv in
+                  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                   (* check if ty is of type *)
                   let w1 = 
                     debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index 6318f489041d48e02e9590c501c53ff1a9e5cee1..b425f219af8585778f7b1a1bcc27fd57c774be39 100644 (file)
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -28,7 +28,7 @@ let constructor_tac ~n ~status:(proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
-    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.MutInd (uri, typeno, exp_named_subst))
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 25c29918fc157097b7cd1bf526dd77ff95073889..12848ad26eb728e63fba02787e6b330888510031 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -29,7 +29,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) =
   let module U = UriManager in
   let module P = PrimitiveTactics in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
       then P.apply_tac 
               ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c1297a0e555eb0cd6cb3bc47dcf76b87fb749096..518c6f86acc5daaa36c3724c2b404276972020dd 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -229,7 +229,7 @@ let apply_tac ~term ~status:(proof, goal) =
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = new_meta_of_proof ~proof in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
@@ -318,7 +318,7 @@ let intros_tac
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let newmeta = new_meta_of_proof ~proof in
     let (context',ty',bo') =
      lambda_abstract context newmeta ty mk_fresh_name_callback
@@ -334,7 +334,7 @@ let cut_tac
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let newmeta1 = new_meta_of_proof ~proof in
    let newmeta2 = newmeta1 + 1 in
    let fresh_name =
@@ -366,7 +366,7 @@ let letin_tac
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let _ = CicTypeChecker.type_of_aux' metasenv context term in
     let newmeta = new_meta_of_proof ~proof in
     let fresh_name =
@@ -389,7 +389,7 @@ let letin_tac
 let exact_tac ~term ~status:(proof, goal) =
  (* Assumption: the term bo must be closed in the current context *)
  let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  let module T = CicTypeChecker in
  let module R = CicReduction in
  if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
@@ -410,7 +410,7 @@ let elim_tac ~term ~status:(proof, goal) =
  let module R = CicReduction in
  let module C = Cic in
   let (curi,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let termty = T.type_of_aux' metasenv context term in
    let uri,exp_named_subst,typeno,args =
     match termty with
@@ -450,7 +450,7 @@ let elim_tac ~term ~status:(proof, goal) =
         (* way.                                                         *)
         let meta_of_corpse =
          let (_,canonical_context,_) =
-          List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
+           CicUtil.lookup_meta (lastmeta - 1) newmetas
          in
           let irl =
            CicMkImplicit.identity_relocation_list_for_metavariable
@@ -549,7 +549,7 @@ exception NotConvertible
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
 let change_tac ~what ~with_what ~status:(proof, goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   (* are_convertible works only on well-typed terms *)
   ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
   if CicReduction.are_convertible context what with_what then

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 07ddf3a9ea4c77c430f3fe5c00d163e6abda76ee..7f4a89fb868bb0da871403047dc7dc4cd922d3a7 100644 (file)
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -33,7 +33,7 @@ let clearbody ~hyp ~status:(proof, goal) =
    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
    | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
       let curi,metasenv,pbo,pty = proof in
-       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+       let metano,_,_ = CicUtil.lookup_meta goal metasenv in
         let string_of_name =
          function
             C.Name n -> n
@@ -98,7 +98,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
    | Some (n_to_clear, _) ->
       let curi,metasenv,pbo,pty = proof in
        let metano,context,ty =
-        List.find (function (m,_,_) -> m=goal) metasenv
+        CicUtil.lookup_meta goal metasenv
        in
         let string_of_name =
          function

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 55eacc234c3da15ffb057255dc73cf30391407f1..5a567b84aa75e6056814d845ea1a35e6d81a6120 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -26,7 +26,7 @@
 (*
 let reduction_tac ~reduction ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let new_ty = reduction context ty in
    let new_metasenv = 
     List.map
@@ -42,7 +42,7 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 (* The default of term is the thesis of the goal to be prooved *)
 let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let terms =
    match terms with None -> [ty] | Some l -> l
   in
@@ -95,7 +95,7 @@ let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
 
 let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let term' = reduction context term in
    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
    (* the type of one metavariable. So we replace it everywhere.   *)

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 8e592e61d842322d4173bc0e0b6dd6420a50abdc..bd9c1513661ba61d6abc8561cbb1ced948e7594e 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -125,20 +125,6 @@ let cic_is_const ?(uri: uri option = None) term =
   *)
 let uri_of_proof ~proof:(uri, _, _, _) = uri
 
-  (**
-    @param metano meta list index
-    @param metasenv meta list (environment)
-    @raise Failure if metano is not found in metasenv
-    @return conjecture corresponding to metano in metasenv
-  *)
-let conj_of_metano metano =
-  try
-    List.find (function (m, _, _) -> m = metano)
-  with Not_found ->
-    failwith (
-      "Ring.conj_of_metano: " ^
-      (string_of_int metano) ^ " no such meta")
-
   (**
     @param status current proof engine status
     @raise Failure if proof is None
@@ -153,7 +139,7 @@ let metasenv_of_status ~status:((_,m,_,_), _) = m
   *)
 let context_of_status ~status:(proof, goal as status) =
   let metasenv = metasenv_of_status ~status:status in
-  let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+  let _, context, _ = CicUtil.lookup_meta goal metasenv in
    context
 
 (** CIC TERM CONSTRUCTORS *)
@@ -448,7 +434,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) =
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in
-    let (_, context, _) = conj_of_metano goal metasenv in
+    let (_, context, _) = CicUtil.lookup_meta goal metasenv in
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
       proof',[goal']
@@ -464,7 +450,7 @@ let ring_tac ~status:((proof, goal) as status) =
   let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
   let r = Reals.r in
   let metasenv = metasenv_of_status ~status in
-  let (metano, context, ty) = conj_of_metano goal metasenv in
+  let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
   match (build_segments ~terms:[t1; t2]) with
   | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 06333d2316582b4615dc4a3618536643539752a5..7270b70b3d5e0be8d09fe1a4f13e7d8a7518be9c 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,7 +40,7 @@ module G = MQueryGenerator
   (* search arguments on which Apply tactic doesn't fail *)
 let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
  let ((_, metasenv, _, _), metano) = status in
- let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
+ let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
   let must = choose_must list_of_must only in
   let result =

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 57660310badd2935b53972670170313f3816b27f..8414698e783f25c0a4da517720caa5602a52e0f9 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -222,7 +222,7 @@ let thens' ~start ~continuations ~status =
 let prova_tac =
  let apply_T_tac ~status:((proof,goal) as status) =
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
    let rel =
     let rec find n =
      function

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 395768db96088a65abb4b63fed6bb5650d665095..04959e6962fdc2bd246db1282ae516682e5c837b 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -33,7 +33,7 @@ let assumption_tac ~status:((proof,goal) as status) =
   let module R = CicReduction in
   let module S = CicSubstitution in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let rec find n = function 
         hd::tl -> 
          (match hd with
@@ -66,7 +66,7 @@ let generalize_tac
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-   let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let _,context,ty = CicUtil.lookup_meta goal metasenv in
     let typ =
      match terms with
         [] -> assert false