Merge pull request coq/ltac2#108 from ejgallego/fix_warn

[coq] Fix OCaml warnings.

10 files changed, 51 insertions, 50 deletions

diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 609e8a6c0e..7b058a339a 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -384,7 +384,7 @@ GRAMMAR EXTEND Gram
   ;
 END
 
-(** Quotation scopes used by notations *)
+(* Quotation scopes used by notations *)
 
 {
 
@@ -866,8 +866,8 @@ end
 
 {
 
-let pr_ltac2entry _ = mt () (** FIXME *)
-let pr_ltac2expr _ = mt () (** FIXME *)
+let pr_ltac2entry _ = mt () (* FIXME *)
+let pr_ltac2expr _ = mt () (* FIXME *)
 
 }
 
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b5ae446ed5..762a145318 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -404,6 +404,8 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_ext Value.val_projection p;
       Value.of_constr c;
     |]
+  | Int _ ->
+    assert false
   end
 end
 
@@ -753,7 +755,7 @@ let () = define1 "hyp" ident begin fun id ->
     let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in
     if mem then return (Value.of_constr (EConstr.mkVar id))
     else Tacticals.New.tclZEROMSG
-      (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (** FIXME: Do something more sensible *)
+      (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (* FIXME: Do something more sensible *)
   end
 end
 
@@ -1082,7 +1084,7 @@ let () =
 
 let () =
   let intern self ist tac =
-    (** Prevent inner calls to Ltac2 values *)
+    (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ist = { ist with Genintern.extra } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
@@ -1113,7 +1115,7 @@ let () =
 let () =
   let open Ltac_plugin in
   let intern self ist tac =
-    (** Prevent inner calls to Ltac2 values *)
+    (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ist = { ist with Genintern.extra } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
@@ -1300,7 +1302,7 @@ end
 
 let () = add_scope "tactic" begin function
 | [] ->
-  (** Default to level 5 parsing *)
+  (* Default to level 5 parsing *)
   let scope = Extend.Aentryl (tac2expr, "5") in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
@@ -1407,7 +1409,7 @@ let rec make_seq_rule = function
   let Seqrule (r, c) = make_seq_rule rem in
   let r = { norec_rule = Next (r.norec_rule, scope.any_symbol) } in
   let f = match tok with
-  | SexprStr _ -> None (** Leave out mere strings *)
+  | SexprStr _ -> None (* Leave out mere strings *)
   | _ -> Some f
   in
   Seqrule (r, CvCns (c, f))
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 22025f0a8f..b7ce363957 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -111,7 +111,7 @@ let push_typedef visibility sp kn (_, def) = match def with
 | GTydDef _ ->
   Tac2env.push_type visibility sp kn
 | GTydAlg { galg_constructors = cstrs } ->
-  (** Register constructors *)
+  (* Register constructors *)
   let iter (c, _) =
     let spc = change_sp_label sp c in
     let knc = change_kn_label kn c in
@@ -120,7 +120,7 @@ let push_typedef visibility sp kn (_, def) = match def with
   Tac2env.push_type visibility sp kn;
   List.iter iter cstrs
 | GTydRec fields ->
-  (** Register fields *)
+  (* Register fields *)
   let iter (c, _, _) =
     let spc = change_sp_label sp c in
     let knc = change_kn_label kn c in
@@ -140,7 +140,7 @@ let define_typedef kn (params, def as qdef) = match def with
 | GTydDef _ ->
   Tac2env.define_type kn qdef
 | GTydAlg { galg_constructors = cstrs } ->
-  (** Define constructors *)
+  (* Define constructors *)
   let constant = ref 0 in
   let nonconstant = ref 0 in
   let iter (c, args) =
@@ -157,7 +157,7 @@ let define_typedef kn (params, def as qdef) = match def with
   Tac2env.define_type kn qdef;
   List.iter iter cstrs
 | GTydRec fs ->
-  (** Define projections *)
+  (* Define projections *)
   let iter i (id, mut, t) =
     let knp = change_kn_label kn id in
     let proj = {
@@ -297,7 +297,7 @@ let inline_rec_tactic tactics =
       let loc = pat.loc in
       (Id.Set.add id avoid, CAst.make ?loc id :: ans)
     in
-    (** Fresh variables to abstract over the function patterns *)
+    (* Fresh variables to abstract over the function patterns *)
     let _, vars = List.fold_left fold_var (avoid, []) pat in
     let map_body ({loc;v=id}, _, e) = CAst.(make ?loc @@ CPatVar (Name id)), e in
     let bnd = List.map map_body tactics in
@@ -656,13 +656,13 @@ let inTac2Abbreviation : abbreviation -> obj =
 
 let register_notation ?(local = false) tkn lev body = match tkn, lev with
 | [SexprRec (_, {loc;v=Some id}, [])], None ->
-  (** Tactic abbreviation *)
+  (* Tactic abbreviation *)
   let () = check_lowercase CAst.(make ?loc id) in
   let body = Tac2intern.globalize Id.Set.empty body in
   let abbr = { abbr_body = body } in
   ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
 | _ ->
-  (** Check that the tokens make sense *)
+  (* Check that the tokens make sense *)
   let entries = List.map ParseToken.parse_token tkn in
   let fold accu tok = match tok with
   | TacTerm _ -> accu
@@ -670,7 +670,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
   | TacNonTerm (Anonymous, _) -> accu
   in
   let ids = List.fold_left fold Id.Set.empty entries in
-  (** Globalize so that names are absolute *)
+  (* Globalize so that names are absolute *)
   let body = Tac2intern.globalize ids body in
   let lev = match lev with Some _ -> lev | None -> Some 5 in
   let ext = {
@@ -758,9 +758,9 @@ let perform_eval e =
   | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
   | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
   | Goal_select.SelectAll -> v
-  | Goal_select.SelectAlreadyFocused -> assert false (** TODO **)
+  | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
   in
-  (** HACK: the API doesn't allow to return a value *)
+  (* HACK: the API doesn't allow to return a value *)
   let ans = ref None in
   let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in
   let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 8198f92ff8..93ad57e97e 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -291,7 +291,7 @@ let is_constructor qid =
   let id = Id.to_string id in
   assert (String.length id > 0);
   match id with
-  | "true" | "false" -> true (** built-in constructors *)
+  | "true" | "false" -> true (* built-in constructors *)
   | _ ->
     match id.[0] with
     | 'A'..'Z' -> true
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index c271967bd6..e3127ab9df 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -349,12 +349,12 @@ let to_fun1 r0 r1 f = to_closure f
 let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic =
   fun arity f args -> match args, arity with
   | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, f)))
-  (** A few hardcoded cases for efficiency *)
+  (* A few hardcoded cases for efficiency *)
   | [a0], OneAty -> f a0
   | [a0; a1], AddAty OneAty -> f a0 a1
   | [a0; a1; a2], AddAty (AddAty OneAty) -> f a0 a1 a2
   | [a0; a1; a2; a3], AddAty (AddAty (AddAty OneAty)) -> f a0 a1 a2 a3
-  (** Generic cases *)
+  (* Generic cases *)
   | a :: args, OneAty ->
     f a >>= fun f ->
     let MLTactic (arity, f) = to_closure f in
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index fe615853ce..de99fb167f 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -141,7 +141,7 @@ let empty_env () = {
 }
 
 let env_name env =
-  (** Generate names according to a provided environment *)
+  (* Generate names according to a provided environment *)
   let mk num =
     let base = num mod 26 in
     let rem = num / 26 in
@@ -267,7 +267,6 @@ let fresh_reftype env (kn : KerName.t or_tuple) =
   (subst, t)
 
 (** First-order unification algorithm *)
-
 let is_unfoldable kn = match snd (Tac2env.interp_type kn) with
 | GTydDef (Some _) -> true
 | GTydDef None | GTydAlg _ | GTydRec _ | GTydOpn -> false
@@ -485,7 +484,7 @@ let check_elt_empty loc env t = match kind env t with
 
 let check_unit ?loc t =
   let env = empty_env () in
-  (** Should not matter, t should be closed. *)
+  (* Should not matter, t should be closed. *)
   let t = fresh_type_scheme env t in
   let maybe_unit = match kind env t with
   | GTypVar _ -> true
@@ -618,7 +617,7 @@ let expand_pattern avoid bnd =
   let fold (avoid, bnd) (pat, t) =
     let na, expand = match pat.v with
     | CPatVar na ->
-      (** Don't expand variable patterns *)
+      (* Don't expand variable patterns *)
       na, None
     | _ ->
       let id = fresh_var avoid in
@@ -691,7 +690,7 @@ let rec intern_rec env {loc;v=e} = match e with
   in
   let e = Tac2env.interp_alias kn in
   let map arg =
-    (** Thunk alias arguments *)
+    (* Thunk alias arguments *)
     let loc = arg.loc in
     let t_unit = CAst.make ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
     let var = CAst.make ?loc @@ CPatCnv (CAst.make ?loc @@ CPatVar Anonymous, t_unit) in
@@ -782,8 +781,8 @@ let rec intern_rec env {loc;v=e} = match e with
     intern_rec env e
   in
   let obj = interp_ml_object tag in
-  (** External objects do not have access to the named context because this is
-      not stable by dynamic semantics. *)
+  (* External objects do not have access to the named context because this is
+     not stable by dynamic semantics. *)
   let genv = Global.env_of_context Environ.empty_named_context_val in
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
@@ -907,7 +906,7 @@ and intern_case env loc e pl =
       | CPatVar Anonymous ->
         let () = check_redundant_clause rem in
         let (br', brT) = intern_rec env br in
-        (** Fill all remaining branches *)
+        (* Fill all remaining branches *)
         let fill (ncst, narg) arity =
           if Int.equal arity 0 then
             let () =
@@ -951,7 +950,7 @@ and intern_case env loc e pl =
           if not (Int.equal nids nargs) then error_nargs_mismatch ?loc knc nargs nids
         in
         let fold env id tpe =
-          (** Instantiate all arguments *)
+          (* Instantiate all arguments *)
           let subst n = GTypVar subst.(n) in
           let tpe = subst_type subst tpe in
           push_name id (monomorphic tpe) env
@@ -1005,7 +1004,7 @@ and intern_case env loc e pl =
         let get = function
         | GPatVar na -> na
         | GPatRef _ ->
-          user_err ?loc (str "TODO: Unhandled match case") (** FIXME *)
+          user_err ?loc (str "TODO: Unhandled match case") (* FIXME *)
         in
         let loc = pat.loc in
         let knc = match knc with
@@ -1024,7 +1023,7 @@ and intern_case env loc e pl =
           if not (Int.equal nids nargs) then error_nargs_mismatch ?loc knc nargs nids
         in
         let fold env id tpe =
-          (** Instantiate all arguments *)
+          (* Instantiate all arguments *)
           let subst n = GTypVar subst.(n) in
           let tpe = subst_type subst tpe in
           push_name id (monomorphic tpe) env
@@ -1089,7 +1088,7 @@ and intern_record env loc fs =
   | _ -> assert false
   in
   let subst = Array.init params (fun _ -> fresh_id env) in
-  (** Set the answer [args] imperatively *)
+  (* Set the answer [args] imperatively *)
   let args = Array.make (List.length typdef) None in
   let iter (loc, pinfo, e) =
     if KerName.equal kn pinfo.pdata_type then
@@ -1145,14 +1144,14 @@ let intern ~strict e =
 
 let intern_typedef self (ids, t) : glb_quant_typedef =
   let env = { (empty_env ()) with env_rec = self } in
-  (** Initialize type parameters *)
+  (* Initialize type parameters *)
   let map id = get_alias id env in
   let ids = List.map map ids in
   let count = ref (List.length ids) in
   let vars = ref UF.Map.empty in
   let iter n id = vars := UF.Map.add id (GTypVar n) !vars in
   let () = List.iteri iter ids in
-  (** Do not accept unbound type variables *)
+  (* Do not accept unbound type variables *)
   let env = { env with env_opn = false } in
   let intern t =
     let t = intern_type env t in
@@ -1195,7 +1194,7 @@ let intern_open_type t =
 let check_subtype t1 t2 =
   let env = empty_env () in
   let t1 = fresh_type_scheme env t1 in
-  (** We build a substitution mimicking rigid variable by using dummy tuples *)
+  (* We build a substitution mimicking rigid variable by using dummy tuples *)
   let rigid i = GTypRef (Tuple (i + 1), []) in
   let (n, t2) = t2 in
   let subst = Array.init n rigid in
@@ -1507,7 +1506,7 @@ let () =
   let intern ist tac =
     let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
-      (** Only happens when Ltac2 is called from a constr or ltac1 quotation *)
+      (* Only happens when Ltac2 is called from a constr or ltac1 quotation *)
       let env = empty_env () in
       if !Ltac_plugin.Tacintern.strict_check then env
       else { env with env_str = false }
@@ -1526,7 +1525,7 @@ let () =
   let intern ist (loc, id) =
     let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
-      (** Only happens when Ltac2 is called from a constr or ltac1 quotation *)
+      (* Only happens when Ltac2 is called from a constr or ltac1 quotation *)
       let env = empty_env () in
       if !Ltac_plugin.Tacintern.strict_check then env
       else { env with env_str = false }
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 6f158ac66e..b0f8083aeb 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -114,7 +114,7 @@ let rec interp (ist : environment) = function
   | Name id -> { env_ist = Id.Map.add id cls accu.env_ist }
   in
   let ist = List.fold_left fold ist fixs in
-  (** Hack to make a cycle imperatively in the environment *)
+  (* Hack to make a cycle imperatively in the environment *)
   let iter (_, e, _) = e.clos_env <- ist.env_ist in
   let () = List.iter iter fixs in
   interp ist e
diff --git a/src/tac2match.mli b/src/tac2match.mli
index 7cfa1ed25f..c82c40d238 100644
--- a/src/tac2match.mli
+++ b/src/tac2match.mli
@@ -28,6 +28,6 @@ val match_goal:
   constr ->
   rev:bool ->
   match_rule ->
-    ((Id.t * context option) list * (** List of hypotheses matching: name + context *)
-    context option * (** Context for conclusion *)
-    Ltac_pretype.patvar_map (** Pattern variable substitution *)) Proofview.tactic
+    ((Id.t * context option) list * (* List of hypotheses matching: name + context *)
+    context option * (* Context for conclusion *)
+    Ltac_pretype.patvar_map (* Pattern variable substitution *)) Proofview.tactic
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 0b20cf9f58..f4cb290265 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -272,7 +272,7 @@ let pr_glbexpr_gen lvl c =
     paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)))
   | GTacExt (tag, arg) ->
     let tpe = interp_ml_object tag in
-    hov 0 (tpe.ml_print (Global.env ()) arg) (** FIXME *)
+    hov 0 (tpe.ml_print (Global.env ()) arg) (* FIXME *)
   | GTacPrm (prm, args) ->
     let args = match args with
     | [] -> mt ()
@@ -379,7 +379,7 @@ let rec pr_valexpr env sigma v t = match kind t with
     else match repr with
     | GTydDef None -> str "<abstr>"
     | GTydDef (Some _) ->
-      (** Shouldn't happen thanks to kind *)
+      (* Shouldn't happen thanks to kind *)
       assert false
     | GTydAlg alg ->
       if Valexpr.is_int v then
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 5a26e7465c..a98264745e 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -233,9 +233,9 @@ let abstract_vars loc vars tac =
   let na, tac = match def with
   | None -> (Anonymous, tac)
   | Some id0 ->
-      (** Trick: in order not to shadow a variable nor to choose an arbitrary
-          name, we reuse one which is going to be shadowed by the matched
-          variables anyways. *)
+      (* Trick: in order not to shadow a variable nor to choose an arbitrary
+         name, we reuse one which is going to be shadowed by the matched
+         variables anyways. *)
       let build_bindings (n, accu) na = match na with
       | Anonymous -> (n + 1, accu)
       | Name _ ->
@@ -263,7 +263,7 @@ let of_conversion {loc;v=c} = match c with
   let vars = pattern_vars pat in
   let pat = of_option ?loc of_pattern (Some pat) in
   let c = of_constr c in
-  (** Order is critical here *)
+  (* Order is critical here *)
   let vars = List.map (fun id -> Name id) (Id.Set.elements vars) in
   let c = abstract_vars loc vars c in
   of_tuple [pat; c]
@@ -388,7 +388,7 @@ let of_constr_matching {loc;v=m} =
       (knd, pat, na)
     in
     let vars = pattern_vars pat in
-    (** Order of elements is crucial here! *)
+    (* Order of elements is crucial here! *)
     let vars = Id.Set.elements vars in
     let vars = List.map (fun id -> Name id) vars in
     let e = abstract_vars loc vars tac in
@@ -429,7 +429,7 @@ let of_goal_matching {loc;v=gm} =
     let hyps = List.map (fun ({CAst.v=na}, _, _, _) -> na) hyps_pats in
     let map (_, na, _, _) = na in
     let hctx = List.map map hyps_pats in
-    (** Order of elements is crucial here! *)
+    (* Order of elements is crucial here! *)
     let vars = Id.Set.elements vars in
     let subst = List.map (fun id -> Name id) vars in
     (r, hyps, hctx, subst, concl_ctx)