Dead code removed.

diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml
index 8f3b13cfda82beef7f3ae2bcbc199965ab792b19..ed4eafb4efd2a39774f331cc1b3d6b78ab31da0d 100644 (file)
--- a/helm/ocaml/acic_content/acic2content.ml
+++ b/helm/ocaml/acic_content/acic2content.ml
@@ -576,7 +576,6 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                K.ArgProof
                 {body with K.proof_name = name; K.proof_context=context} in
           List.map2 build_proof patterns name_and_arities in
-        let teid = get_id te in
         let context,term =
           (match 
              build_subproofs_and_args 

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f03752d10b10ec1cdec64077546206dbcead7af8..f01ecf785ed8524f5002d6c3f6e08610a617bdbb 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -853,7 +853,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 
   and  avoid_double_coercion subst metasenv ugraph t ty = 
     match t with
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
           let source_carr = CoercGraph.source_of c2 in
           let tgt_carr = CicMetaSubst.apply_subst subst ty in

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index fe631edd2e761579b8d70c27c24490f87c861d4a..922955aa0af384c3e16716c8942c2097d225426a 100644 (file)
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -50,7 +50,7 @@ let merge_coercions obj =
         C.Lambda (name, aux so, aux dest)
     | C.LetIn (name,so,dest) -> 
         C.LetIn (name, aux so, aux dest)
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
         let source_carr = CoercGraph.source_of c2 in
         let tgt_carr = CoercGraph.target_of c1 in
@@ -180,7 +180,7 @@ let index_obj =
 
 let add_single_obj uri obj ~basedir =
   let obj = 
-    if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
+    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
     then
       merge_coercions obj 

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8304d7bb19264738127e76f6409988d69ab14934..b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -67,14 +67,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in
-       let last_hyp_name_of_status (proof,goal) =
-        let curi, metasenv, pbo, pty = proof in
-        let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-         match context with
-            (Some (Cic.Name s,_))::_ -> s
-          | _ -> assert false
-       in
-        let dummy = "dummy" in
+       let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
            Tacticals.seq

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 5418e114935cc4af1f0742be18cd64634b70ac75..8b910bded8ebabe6c5695016930b4ef4325c721b 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -196,8 +196,8 @@ let rational_of_const = rational_of_term;;
 *)
 let fails f a =
  try
-   let tmp = (f a) in
-   false
+  ignore (f a);
+  false
  with 
    _-> true
  ;;
@@ -662,11 +662,7 @@ let tac_zero_inf_false gl (n,d) =
     apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
    else
     apply_tactic (Tacticals.then_ 
-     ~start:( mk_tactic (fun status -> 
-       let (proof, goal) = status in
-       let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+     ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt)))
      ~continuation:(tac_zero_infeq_pos gl (-n,d))) 
     status
  in

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 755a098547eb4e6d13c75ed1c807c888727d5151..cc5af63ae3558aaa7feb7697d59f3b67b386be84 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -695,18 +695,16 @@ let simpl context =
               in
                reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
              let (_,_,body) = List.nth fl i in
-              let body' =
-               let counter = ref (List.length fl) in
-                List.fold_right
-                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                 fl
-                 body
-              in
-               let tl' = List.map (reduceaux context []) tl in
-                reduceaux context tl' body'
+             let body' =
+              let counter = ref (List.length fl) in
+               List.fold_right
+                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                fl
+                body
+             in
+              let tl' = List.map (reduceaux context []) tl in
+               reduceaux context tl' body'
          | t -> t
        in
         (match decofix (CicReduction.whd context term) with