removing a few warnings

common.v

@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 (** coercion from sums to Booleans  *)
-Fixpoint bool_of_sumbool A B (c: sumbool A B): bool := if c then true else false.
+Definition bool_of_sumbool A B (c: sumbool A B): bool := if c then true else false.
 Coercion bool_of_sumbool: sumbool >-> bool.
 
 Lemma sumbool_true A (c: sumbool A (~A)): A -> c.

comparisons.v

@@ -139,19 +139,21 @@ Canonical Structure cmp_nat := mk_cmp _ eqb_nat_spec _ nat_compare_spec.
 
 
 (** * Booleans as a [cmpType] *)
-Fixpoint eqb_bool i j := 
+Definition eqb_bool i j := 
   match i,j with 
     | false,false | true,true => true
     | _,_ => false
   end.
+Arguments eqb_bool !i !j/.
 Lemma eqb_bool_spec: forall i j, reflect (i=j) (eqb_bool i j).
 Proof. destruct i; destruct j; constructor; congruence. Qed.
-Fixpoint bool_compare i j := 
+Definition bool_compare i j := 
   match i,j with 
     | false,false | true,true => Eq
     | false,true => Lt
     | true,false => Gt
   end.
+Arguments bool_compare !i !j/.
 Lemma bool_compare_spec: forall i j, compare_spec (i=j) (bool_compare i j).
 Proof. destruct i; destruct j; constructor; congruence. Qed.
 Canonical Structure cmp_bool := mk_cmp _ eqb_bool_spec _ bool_compare_spec.

mrewrite.mlg

@@ -106,7 +106,7 @@ let extend ist k dir h =
       | Prod(x,s,t) -> mkLambda(x,s,ext (push x s env) (i-1) (mkApp(h,[|mkRel i|])) t)
       | _ -> error "the provided term does not end with a relation algebra (in)equation"
   in
-  let t = Tacmach.New.pf_unsafe_type_of goal h in
+  let _,t = Tacmach.New.pf_type_of goal h in
   let h = ext (Proofview.Goal.env goal) (length !sigma t) h t in
   (* Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS !sigma) *)
   (ltac_apply ist k h)

ra_common.ml

@@ -51,7 +51,7 @@ let convertible' (env,sigma) = Reductionops.is_conv env sigma
 (* in a given goal *)
 let convertible = Tacmach.pf_conv_x
 
-(* creating a name a reference to that name *)
+(* creating a name and a reference to that name *)
 let fresh_name n goal =
   let vname = Tactics.fresh_id Id.Set.empty (Id.of_string n) goal in
     Context.annotR vname, mkVar vname

ra_fold.mlg

@@ -25,7 +25,7 @@ open Proofview
 
 let ra_fold_term ops ob t goal =
   let env = Tacmach.pf_env goal in
-  let tops = Tacmach.pf_unsafe_type_of goal ops in
+  let _,tops = Tacmach.pf_type_of goal ops in
   let rec fill sigma ops tops =
     if EConstr.eq_constr sigma tops (Lazy.force Monoid.ops) then (sigma,ops)
     else
@@ -90,7 +90,7 @@ let ra_fold_term ops ob t goal =
       | _ -> e
 
   and fold env e =
-    let t = Typing.unsafe_type_of env !sigma e in
+    let _,t = Typing.type_of env !sigma e in
     match ob with
       | Some o when convertible' (env,!sigma) t (Lattice.car (Monoid.mor ops o o)) -> ra_fold env o o e
       | Some o when EConstr.eq_constr !sigma t mkProp ->