From afa05d30f20de12e031c3e5c3e5c33c19c42a7d8 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sun, 27 Nov 2005 16:17:59 +0000
Subject: [PATCH] removed deadcode / fixed typos (thanks to ocaml 3.09)

---
 helm/ocaml/acic_content/termAcicContent.ml    |  2 +-
 helm/ocaml/cic/cicUniv.ml                     |  2 +-
 helm/ocaml/cic/unshare.ml                     |  2 -
 helm/ocaml/cic_acic/doubleTypeInference.ml    |  2 +-
 helm/ocaml/cic_acic/eta_fixing.ml             |  6 +--
 helm/ocaml/cic_disambiguation/disambiguate.ml |  1 -
 .../cic_disambiguation/number_notation.ml     |  3 --
 .../cic_proof_checking/cicEnvironment.ml      |  4 +-
 helm/ocaml/cic_proof_checking/cicReduction.ml | 10 ++---
 .../cic_proof_checking/cicSubstitution.ml     |  4 +-
 .../cic_proof_checking/cicTypeChecker.ml      | 12 +++---
 helm/ocaml/cic_unification/cicRefine.ml       |  1 -
 helm/ocaml/content_pres/boxPp.ml              |  2 +-
 helm/ocaml/content_pres/cicNotationLexer.ml   |  4 +-
 helm/ocaml/content_pres/cicNotationParser.ml  |  2 +-
 helm/ocaml/content_pres/cicNotationPres.ml    |  4 +-
 .../ocaml/content_pres/content2presMatcher.ml |  2 +-
 helm/ocaml/content_pres/termContentPres.ml    |  2 +-
 helm/ocaml/tactics/autoTactic.ml              | 17 ++-------
 helm/ocaml/tactics/discriminationTactics.ml   |  2 +-
 helm/ocaml/tactics/equalityTactics.ml         |  2 +-
 helm/ocaml/tactics/fourierR.ml                |  2 -
 helm/ocaml/tactics/metadataQuery.ml           |  8 ++--
 helm/ocaml/tactics/proofEngineHelpers.ml      |  2 -
 helm/ocaml/tactics/proofEngineReduction.ml    | 38 +++++--------------
 25 files changed, 45 insertions(+), 91 deletions(-)

diff --git a/helm/ocaml/acic_content/termAcicContent.ml b/helm/ocaml/acic_content/termAcicContent.ml
index a9cf9a4d1..4cab1346c 100644
--- a/helm/ocaml/acic_content/termAcicContent.ml
+++ b/helm/ocaml/acic_content/termAcicContent.ml
@@ -119,7 +119,7 @@ let ast_of_acic0 term_info acic k =
     | Cic.AConst (id,uri,substs) ->
         register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
-    | Cic.AMutInd (id,uri,i,substs) as t ->
+    | Cic.AMutInd (id,uri,i,substs) ->
         let name = name_of_inductive_type uri i in
         let uri_str = UriManager.string_of_uri uri in
         let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in
diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 3d92f3335..1ab577ec8 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -420,7 +420,7 @@ let fill_empty_nodes_with_uri g l uri =
   let fill_empty_set s =
     SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty 
   in
-  let fill_empty_entry e = { e with
+  let fill_empty_entry e = {
     eq_closure = (fill_empty_set e.eq_closure) ;
     ge_closure = (fill_empty_set e.ge_closure) ;
     gt_closure = (fill_empty_set e.gt_closure) ;
diff --git a/helm/ocaml/cic/unshare.ml b/helm/ocaml/cic/unshare.ml
index 9300c9e3a..522c82562 100644
--- a/helm/ocaml/cic/unshare.ml
+++ b/helm/ocaml/cic/unshare.ml
@@ -67,7 +67,6 @@ let rec unshare =
       C.MutCase (sp, i, unshare outty, unshare t,
        List.map unshare pl)
    | C.Fix (i, fl) ->
-      let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo))
@@ -75,7 +74,6 @@ let rec unshare =
       in
        C.Fix (i, liftedfl)
    | C.CoFix (i, fl) ->
-      let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, ty, bo) -> (name, unshare ty, unshare bo))
diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml
index b28359bd7..98d12ceca 100644
--- a/helm/ocaml/cic_acic/doubleTypeInference.ml
+++ b/helm/ocaml/cic_acic/doubleTypeInference.ml
@@ -114,7 +114,7 @@ let rec beta_reduce =
        let exp_named_subst' =
         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
-        C.Var (uri,exp_named_subst)
+        C.Var (uri,exp_named_subst')
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
diff --git a/helm/ocaml/cic_acic/eta_fixing.ml b/helm/ocaml/cic_acic/eta_fixing.ml
index 68dec37d6..75e66d934 100644
--- a/helm/ocaml/cic_acic/eta_fixing.ml
+++ b/helm/ocaml/cic_acic/eta_fixing.ml
@@ -200,7 +200,7 @@ let eta_fix metasenv context t =
    | C.LetIn (n,s,t) -> 
        C.LetIn 
         (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
-   | C.Appl l as appl -> 
+   | C.Appl l -> 
        let l' =  List.map (eta_fix' context) l 
        in 
        (match l' with
@@ -232,7 +232,7 @@ let eta_fix metasenv context t =
    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
        let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.MutConstruct (uri, tyno, consno, exp_named_subst')
-   | C.MutCase (uri, tyno, outty, term, patterns) as prima ->
+   | C.MutCase (uri, tyno, outty, term, patterns) ->
        let outty' =  eta_fix' context outty in
        let term' = eta_fix' context term in
        let patterns' = List.map (eta_fix' context) patterns in
@@ -274,7 +274,7 @@ let eta_fix metasenv context t =
              | _ -> prerr_endline ("QUA"); assert false) in 
        let patterns2 = 
          List.map2 fix_lambdas_wrt_type
-           constructor_types patterns in 
+           constructor_types patterns' in 
          C.MutCase (uri, tyno, outty',term',patterns2)
    | C.Fix (funno, funs) ->
        let fun_types = 
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index ce26f9351..fd8e2a799 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -767,7 +767,6 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       let todo_dom = domain_diff thing_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
-        let id_choices = Hashtbl.create 1023 in
         fun item ->
           let choices =
             let lookup_in_library () =
diff --git a/helm/ocaml/cic_disambiguation/number_notation.ml b/helm/ocaml/cic_disambiguation/number_notation.ml
index 09f488e86..05800ffac 100644
--- a/helm/ocaml/cic_disambiguation/number_notation.ml
+++ b/helm/ocaml/cic_disambiguation/number_notation.ml
@@ -24,9 +24,6 @@
  *)
 
 let _ =
-  let const s = Cic.Const (s, []) in
-  let mutind s = Cic.MutInd (s, 0, []) in
-
   DisambiguateChoices.add_num_choice
     ("natural number",
       (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 2849bc38a..8a9bbf667 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -203,7 +203,6 @@ module Cache :
             C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
              List.map restore_in_term pl)
          | C.Fix (i, fl) ->
-            let len = List.length fl in
             let liftedfl =
              List.map
               (fun (name, i, ty, bo) ->
@@ -212,7 +211,6 @@ module Cache :
             in
              C.Fix (i, liftedfl)
          | C.CoFix (i, fl) ->
-            let len = List.length fl in
             let liftedfl =
              List.map
               (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo))
@@ -576,7 +574,7 @@ let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
  * return the object,ugraph
  *)
 let add_trusted_uri_to_cache uri = 
-  let o,u,_ = find_or_add_to_unchecked uri in
+  let _ = find_or_add_to_unchecked uri in
   Cache.unchecked_to_frozen uri;
   set_type_checking_info uri;
   try
diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 813a589d6..7ba2cffbc 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -526,7 +526,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
    let module S = CicSubstitution in 
    let rec reduce =
     function
-       (k, e, _, (C.Rel n as t), s) ->
+       (k, e, _, C.Rel n, s) ->
         let d =
          try
           Some (RS.from_env (List.nth e (n-1)))
@@ -577,14 +577,14 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
-     | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+     | (k, e, ens, C.Cast (te,ty), s) ->
         reduce (k, e, ens, te, s) (* s should be empty *)
      | (k, e, ens, (C.Prod _ as t), s) ->
          unwind k e ens t (* s should be empty *)
      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
-     | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+     | (k, e, ens, C.LetIn (_,m,t), s) ->
         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
          reduce (k+1, m'::e, ens, t, s)
      | (_, _, _, C.Appl [], _) -> assert false
@@ -641,7 +641,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
         let decofix =
          function
-            C.CoFix (i,fl) as t ->
+            C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -1077,7 +1077,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   let t = whd ~delta ~subst ctx term in
   let aux = normalize ~delta ~subst in
   let decl name t = Some (name, C.Decl t) in
-  let def  name t = Some (name, C.Def (t,None)) in
+  let def name t = Some (name, C.Def (t,None)) in
   match t with
   | C.Rel n -> t
   | C.Var (uri,exp_named_subst) ->
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index a9fa1d9b1..e9ce94eb8 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -121,7 +121,7 @@ let subst arg =
         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
@@ -230,7 +230,7 @@ debug_print (lazy "---- END\n\n ") ;
 *)
             C.Var (uri,exp_named_subst'')
        )
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index af98ff0ef..239bd4415 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -66,7 +66,7 @@ let debrujin_constructor uri number_of_types =
         C.Var (uri,exp_named_subst')
     | C.Meta (i,l) ->
        let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
-        C.Meta (i,l)
+        C.Meta (i,l')
     | C.Sort _
     | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
@@ -545,7 +545,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 		ugraph'
             ) ugraph cl in
 	(i + 1),ugraph''
-      ) itl (1,ugraph)
+      ) itl (1,ugrap1)
   in
   ugraph2
 
@@ -1126,11 +1126,10 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
          | C.Lambda _
          | C.LetIn _ ->
             raise (AssertFailure (lazy "25"))(* due to type-checking *)
-         | C.Appl ((C.MutInd (uri,_,_))::_) as ty
-            when uri == coInductiveTypeURI -> 
+         | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> 
              guarded_by_constructors ~subst context n nn true te []
               coInductiveTypeURI
-         | C.Appl ((C.MutInd (uri,_,_))::_) as ty -> 
+         | C.Appl ((C.MutInd (uri,_,_))::_) -> 
             guarded_by_constructors ~subst context n nn true te tl
              coInductiveTypeURI
          | C.Appl _ ->
@@ -1687,8 +1686,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		  (lazy (sprintf
 		      ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
 		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
-          | C.Appl 
-	      ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
               if U.eq uri uri' && i = i' then
 		let params,args =
 		  split tl (List.length tl - k)
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 6d28ca177..661d5c34c 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1122,7 +1122,6 @@ let map_first_n n start f g l =
    
 (*CSC: this is a very rough approximation; to be finished *)
 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
-  let number_of_types = List.length tys in
   let subst,metasenv,ugraph,tys = 
     List.fold_right
       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
diff --git a/helm/ocaml/content_pres/boxPp.ml b/helm/ocaml/content_pres/boxPp.ml
index ddb9d3b82..657f8a9d3 100644
--- a/helm/ocaml/content_pres/boxPp.ml
+++ b/helm/ocaml/content_pres/boxPp.ml
@@ -130,7 +130,7 @@ let render_to_strings size markup =
           let tl_renderings =
             List.map
               (fun f ->
-                let indent_header = if indent then string_indent else "" in
+(*                 let indent_header = if indent then string_indent else "" in *)
                 snd (indent_children (f children_size)))
               tl_fs
           in
diff --git a/helm/ocaml/content_pres/cicNotationLexer.ml b/helm/ocaml/content_pres/cicNotationLexer.ml
index 33fb8fd78..958b246de 100644
--- a/helm/ocaml/content_pres/cicNotationLexer.ml
+++ b/helm/ocaml/content_pres/cicNotationLexer.ml
@@ -302,7 +302,7 @@ and level2_ast_token =
         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
   | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
   | beginnote -> 
-      let comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
+      let _comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
 (*       let comment =
         Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
       in
@@ -347,5 +347,5 @@ let lookup_ligatures lexeme =
     if lexeme.[0] = '\\'
     then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ]
     else List.rev (Hashtbl.find_all ligatures lexeme)
-  with Invalid_argument _ | Utf8Macro.Macro_not_found _ as exn -> []
+  with Invalid_argument _ | Utf8Macro.Macro_not_found _ -> []
 
diff --git a/helm/ocaml/content_pres/cicNotationParser.ml b/helm/ocaml/content_pres/cicNotationParser.ml
index 71cc2bffd..066eb813f 100644
--- a/helm/ocaml/content_pres/cicNotationParser.ml
+++ b/helm/ocaml/content_pres/cicNotationParser.ml
@@ -231,7 +231,7 @@ let extend level1_pattern ~precedence ~associativity action =
     List.split (extract_term_production level1_pattern)
   in
   let level = level_of precedence associativity in
-  let p_names = flatten_opt p_bindings in
+(*   let p_names = flatten_opt p_bindings in *)
   let _ =
     Grammar.extend
       [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
diff --git a/helm/ocaml/content_pres/cicNotationPres.ml b/helm/ocaml/content_pres/cicNotationPres.ml
index cc3a204a4..3e47cceb9 100644
--- a/helm/ocaml/content_pres/cicNotationPres.ml
+++ b/helm/ocaml/content_pres/cicNotationPres.ml
@@ -199,7 +199,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t =
 let render ids_to_uris =
   let module A = Ast in
   let module P = Mpresentation in
-  let use_unicode = true in
+(*   let use_unicode = true in *)
   let lookup_uri id =
     (try
       let uri = Hashtbl.find ids_to_uris id in
@@ -304,7 +304,7 @@ let render ids_to_uris =
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
     let new_pos = ref pos in
-    let reinit = ref false in
+(*     let reinit = ref false in *)
     let rec aux_attribute =
       function
       | A.AttributedTerm (attr, t) ->
diff --git a/helm/ocaml/content_pres/content2presMatcher.ml b/helm/ocaml/content_pres/content2presMatcher.ml
index 9a2f0d20b..4d99040d5 100644
--- a/helm/ocaml/content_pres/content2presMatcher.ml
+++ b/helm/ocaml/content_pres/content2presMatcher.ml
@@ -56,7 +56,7 @@ struct
       | Ast.Variable _ -> PatternMatcher.Variable
       | Ast.Magic _
       | Ast.Layout _
-      | Ast.Literal _ as t -> assert false
+      | Ast.Literal _ -> assert false
       | _ -> PatternMatcher.Constructor
     let tag_of_pattern = get_tag
     let tag_of_term t = get_tag t
diff --git a/helm/ocaml/content_pres/termContentPres.ml b/helm/ocaml/content_pres/termContentPres.ml
index 3236fb433..fedcef6af 100644
--- a/helm/ocaml/content_pres/termContentPres.ml
+++ b/helm/ocaml/content_pres/termContentPres.ml
@@ -289,7 +289,7 @@ let instantiate21 idrefs env l1 =
         Ast.AttributedTerm (attr, subst_singleton pos env t)
     | t -> CicNotationUtil.group (subst pos env t)
   and subst pos env = function
-    | Ast.AttributedTerm (attr, t) as term ->
+    | Ast.AttributedTerm (attr, t) ->
 (*         prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
         subst pos env t
     | Ast.Variable var ->
diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index b232d9894..03dd1f254 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -120,13 +120,6 @@ let new_search_theorems f dbd proof goal depth sign =
 
 exception NoOtherChoices;;
 
-let is_in_metasenv goal metasenv =
-  try
-    let (_, ey ,ty) =
-      CicUtil.lookup_meta goal metasenv in
-      true
-  with CicUtil.Meta_not_found _ -> false 
-
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
  universe
   =
@@ -137,7 +130,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   let _,metasenv,p,_ = proof in
     (* first of all we check if the goal has been already
        inspected *)
-  assert (is_in_metasenv goal metasenv);
+  assert (CicUtil.exists_meta goal metasenv);
   let exitus =
     try Hashtbl.find inspected_goals ty
     with Not_found -> NotYetInspected in
@@ -234,13 +227,9 @@ and auto_new dbd width already_seen_goals universe = function
   | [] -> []
   | (subst,(proof, goals, sign))::tl ->
       let _,metasenv,_,_ = proof in
-      let is_in_metasenv (goal, _) =
-        try
-          let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
-          true
-        with CicUtil.Meta_not_found _ -> false 
+      let goals'=
+        List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
-      let goals'= List.filter is_in_metasenv goals in
     	auto_new_aux dbd 
         width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 
diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index c9feaaee6..dd122ee48 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -59,7 +59,7 @@ let rec injection_tac ~term =
                              T.then_ 
                               ~start:(injection1_tac ~i ~term)
                               ~continuation:(traverse_list (i+1) tl1 tl2)
-                          | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac
+                          | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
                        in traverse_list 1 applist1 applist2
                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 7ed946170..a8e328863 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -35,7 +35,7 @@ let rec rewrite_tac ~direction ~pattern equality =
   assert (wanted = None);   (* this should be checked syntactically *)
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
-  let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic
diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 13dd9f410..32dfb5db2 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -941,8 +941,6 @@ let rec fourier (s_proof,s_goal)=
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
   debug_pcontext s_context;
 
-  let fhyp = String.copy "new_hyp_for_fourier" in 
-   
 (* here we need to negate the thesis, but to do this we need to apply the 
    right theoreme,so let's parse our thesis *)
   
diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 535509a88..9385f1c99 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -170,7 +170,7 @@ let cmatch' =
 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
@@ -188,14 +188,14 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   uris
 
-let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
-  let to_string set =
+let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+(*   let to_string set =
     "{ " ^
       (String.concat ", "
          (Constr.UriManagerSet.fold
             (fun u l -> (UriManager.string_of_uri u)::l) set []))
     ^ " }"
-  in
+  in *)
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index fd336910e..a5541ab03 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -301,7 +301,6 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     List.concat (map2 "wrong number of arguments in application"
       (fun t1 t2 -> aux context t1 t2) terms1 terms2)
   in
-   let context_len = List.length context in
    let roots = aux context where term in
     match wanted with
        None -> [],metasenv,ugraph,roots
@@ -482,7 +481,6 @@ exception Fail of string Lazy.t
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
-   let context_len = List.length context in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 62c2adab5..0a1f13a78 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -206,7 +206,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
@@ -298,14 +298,14 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     S.lift (k-1) (find_image t)
    with Not_found ->
     match t with
-       C.Rel n as t ->
+       C.Rel n ->
         if n < k then C.Rel n else C.Rel (n + nnn)
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
         in
          C.Var (uri,exp_named_subst')
-     | C.Meta (i, l) as t -> 
+     | C.Meta (i, l) -> 
         let l' =
          List.map
           (function
@@ -450,7 +450,7 @@ let reduce context =
        in
         let t' = C.MutInd (uri,i,exp_named_subst') in
          if l = [] then t' else C.Appl (t'::l)
-    | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
@@ -459,10 +459,7 @@ let reduce context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
-            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -473,9 +470,6 @@ let reduce 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
@@ -600,14 +594,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let mk_appl t l =
-   if l = [] then 
-     t 
-   else 
-     match t with
-     | Cic.Appl l' -> Cic.Appl (l'@l)
-     | _ -> Cic.Appl (t::l)
- in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
@@ -697,9 +683,7 @@ let simpl context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -721,7 +705,7 @@ let simpl context =
                  body
               in
                let tl' = List.map (reduceaux context []) tl in
-                reduceaux context tl body'
+                reduceaux context tl' body'
          | t -> t
        in
         (match decofix (CicReduction.whd context term) with
@@ -818,7 +802,7 @@ let simpl context =
     let res,constant_args =
      let rec aux rev_constant_args l =
       function
-         C.Lambda (name,s,t) as t' ->
+         C.Lambda (name,s,t) ->
           begin
            match l with
               [] -> raise WrongShape
@@ -829,11 +813,7 @@ let simpl context =
           end
        | C.LetIn (_,s,t) ->
           aux rev_constant_args l (S.subst s t)
-       | C.Fix (i,fl) as t ->
-          let tys =
-           List.map (function (name,_,ty,_) ->
-            Some (C.Name name, C.Decl ty)) fl
-          in
+       | C.Fix (i,fl) ->
            let (_,recindex,_,body) = List.nth fl i in
             let recparam =
              try
-- 
2.39.2