Merge branch 'v8.5'

2 files changed, 4 insertions, 4 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 9a19d4bda7..2dfebc9a3c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -407,7 +407,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in
+    let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 539c2ab713..59a7168e51 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3252,7 +3252,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
 	mkProd (Anonymous, eq, lift 1 concl), [| refl |]
     else concl, [||]
   in
-    (* Abstract by equalitites *)
+    (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
   let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
     (* Abstract by the "generalized" hypothesis. *)
@@ -3263,11 +3263,11 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in
     (* Apply the old arguments giving the proper instantiation of the hyp *)
   let instc = mkApp (genc, Array.of_list args) in
-    (* Then apply to the original instanciated hyp. *)
+    (* Then apply to the original instantiated hyp. *)
   let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in
     (* Apply the reflexivity proofs on the indices. *)
   let appeqs = mkApp (instc, Array.of_list refls) in
-    (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
+    (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
   Sigma (mkApp (appeqs, abshypt), sigma, p)
   end }