Addressing OCaml compilation warnings.

One of them revealed a true bug.

5 files changed, 5 insertions, 6 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 1262864c7..1f29a2948 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function
       e', PatCstr (loc,cstr,patl',na')
 
 let subst_binder_type_vars l = function
-  | Evar_kinds.BinderType (Name id) as e ->
+  | Evar_kinds.BinderType (Name id) ->
      let id =
        try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
        with Not_found -> id in
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 65d49cb45..a292c7463 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -449,7 +449,6 @@ let extend_constr state forpat ng =
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
-    let nb_decls = List.length needed_levels + 1 in
     let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
     let empty = { constrs = []; constrlists = []; binders = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index ff1db8cf5..a34fa4cae 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -903,7 +903,7 @@ let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
-  | k, (_, Some c) as x -> k, 
+  | k, (_, Some c) -> k,
       let x = Tacintern.intern_constr gs c in
       fst x, Some c
   | ct -> ct
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e2c78a507..f3117db17 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -802,7 +802,7 @@ module Make
       let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
       let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
 
-      let pr_constrarg c = spc () ++ pr.pr_constr c in
+      let _pr_constrarg c = spc () ++ pr.pr_constr c in
       let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
       let pr_intarg n = spc () ++ int n in
 
@@ -850,7 +850,7 @@ module Make
                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
                   pr_lconstrarg ty ++ str")") in
       (*  spc() ++
-          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
           c)
       *)
       let pr_cofix_tac (id,c) =
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc469..7b52a9cee 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -509,7 +509,7 @@ let coq_eqdec ~sum ~rev =
     let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
     let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
     let args = if rev then List.rev args else args in
-    mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]])
+    mkPattern (mkGAppRef sum args)
   )
 
 (** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)