9 files changed, 23 insertions, 23 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 0e7804bc7d..7401756886 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -232,7 +232,7 @@ let rec norm_head info env t stack =
 	let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
         norm_head info env' c stack
       else
-	(CBN(t,env), stack) (* Considérer une coupure commutative ? *)
+	(CBN(t,env), stack) (* Should we consider a commutative cut ? *)
 
   | Evar ev ->
       (match evar_value info.i_cache ev with
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ae1c4eea0c..54621eb9d5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -399,7 +399,7 @@ type coercion = {
   coercion_params : int;
 }
 
-(* Calcul de l'arité d'une classe *)
+(* Computation of the class arity *)
 
 let reference_arity_length ref =
   let t = Universes.unsafe_type_of_global ref in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 504d73cb87..ae9210e494 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -9,7 +9,7 @@
 (* Created by Hugo Herbelin for Coq V7 by isolating the coercion
    mechanism out of the type inference algorithm in file trad.ml from
    Coq V6.3, Nov 1999; The coercion mechanism was implemented in
-   trad.ml by Amokrane Saïbi, May 1996 *)
+   trad.ml by Amokrane Saïbi, May 1996 *)
 (* Addition of products and sorts in canonical structures by Pierre
    Corbineau, Feb 2008 *)
 (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
@@ -345,7 +345,7 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
-(* appliquer le chemin de coercions p à hj *)
+(* appliquer le chemin de coercions p à hj *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7a1f155bd4..27c1e1e7c5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -180,11 +180,11 @@ let computable p k =
        A solution could be to store, in the MutCase, the eta-expanded
        normal form of pred to decide if it depends on its variables
 
-       Lorsque le prédicat est dépendant de manière certaine, on
-       ne déclare pas le prédicat synthétisable (même si la
-       variable dépendante ne l'est pas effectivement) parce que
-       sinon on perd la réciprocité de la synthèse (qui, lui,
-       engendrera un prédicat non dépendant) *)
+       Lorsque le prédicat est dépendant de manière certaine, on
+       ne déclare pas le prédicat synthétisable (même si la
+       variable dépendante ne l'est pas effectivement) parce que
+       sinon on perd la réciprocité de la synthèse (qui, lui,
+       engendrera un prédicat non dépendant) *)
 
   let sign,ccl = decompose_lam_assum p in
   Int.equal (rel_context_length sign) (k + 1)
@@ -644,7 +644,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
 
       | _, false::l ->
             (* eta-expansion : n'arrivera plus lorsque tous les
-               termes seront construits à partir de la syntaxe Cases *)
+               termes seront construits à partir de la syntaxe Cases *)
             (* nommage de la nouvelle variable *)
 	    let new_b = applist (lift 1 b, [mkRel 1]) in
             let pat,new_avoid,new_env,new_ids =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index cce0ff5eca..661aa8b7a8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -73,8 +73,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   in
   let ndepar = mip.mind_nrealdecls + 1 in
 
-  (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
-  (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
+  (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
+  (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
 
@@ -241,7 +241,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
     in
     prec env 0 []
   in
-  (* ici, cstrprods est la liste des produits du constructeur instantié *)
+  (* ici, cstrprods est la liste des produits du constructeur instantié *)
   let rec process_constr env i f = function
     | (n,None,t as d)::cprest, recarg::rest ->
         let optionpos =
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index a6c0149a4e..ed4bc4d394 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -176,8 +176,8 @@ let next_ident_away_from id bad =
 
 let restart_subscript id =
   if not (has_subscript id) then id else
-    (* Ce serait sans doute mieux avec quelque chose inspiré de
-     *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+    (* It would probably be better with something in the spirit of
+     *** make_ident id (Some 0) *** but compatibility would be lost... *)
     forget_subscript id
 
 let rec to_avoid id = function
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0576ec57ba..afb1c94759 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -325,7 +325,7 @@ let rec pat_of_raw metas vars = function
       metas := n::!metas; PMeta (Some n)
   | GRef (_,gr,_) ->
       PRef (canonical_gr gr)
-  (* Hack pour ne pas réécrire une interprétation complète des patterns*)
+  (* Hack to avoid rewriting a complete interpretation of patterns *)
   | GApp (_, GPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
   | GApp (_,c,cl) ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 66aa85ecd9..f836c2327e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Created by Amokrane Saïbi, Dec 1998 *)
+(* Created by Amokrane Saïbi, Dec 1998 *)
 (* Addition of products and sorts in canonical structures by Pierre
    Corbineau, Feb 2008 *)
 
@@ -28,10 +28,10 @@ open Reductionops
    constructor (the name of which defaults to Build_S) *)
 
 (* Table des structures: le nom de la structure (un [inductive]) donne
-   le nom du constructeur, le nombre de paramètres et pour chaque
-   argument réel du constructeur, le nom de la projection
-   correspondante, si valide, et un booléen disant si c'est une vraie
-   projection ou bien une fonction constante (associée à un LetIn) *)
+   le nom du constructeur, le nombre de paramètres et pour chaque
+   argument réel du constructeur, le nom de la projection
+   correspondante, si valide, et un booléen disant si c'est une vraie
+   projection ou bien une fonction constante (associée à un LetIn) *)
 
 type struc_typ = {
   s_CONST : constructor;
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 75c8fb4246..72f87a19ea 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -851,9 +851,9 @@ let align_prod_letin c a : rel_context * constr =
   let (l1,l2) = Util.List.chop lc l in
   l2,it_mkProd_or_LetIn a l1
 
-(* On reduit une serie d'eta-redex de tete ou rien du tout  *)
+(* We reduce a series of head eta-redex or nothing at all   *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
-(* Remplace 2 versions précédentes buggées                  *)
+(* Remplace 2 earlier buggish versions                      *)
 
 let rec eta_reduce_head c =
   match kind_of_term c with