Switch the few remaining iso-latin-1 files to utf8

14 files changed, 145 insertions, 154 deletions

diff --git a/plugins/cc/README b/plugins/cc/README
index 073b140ea..c616b5daa 100644
--- a/plugins/cc/README
+++ b/plugins/cc/README
@@ -3,7 +3,7 @@ cctac: congruence-closure for coq
 
 author: Pierre Corbineau, 
 	Stage de DEA au LSV, ENS Cachan
-	Thèse au LRI, Université Paris Sud XI 
+	Thèse au LRI, Université Paris Sud XI 
 
 Files :
 
diff --git a/plugins/extraction/README b/plugins/extraction/README
index a9a7b04d5..458ba0deb 100644
--- a/plugins/extraction/README
+++ b/plugins/extraction/README
@@ -14,7 +14,7 @@ Who did it ?
 ------------
 
 The current implementation (from version 7.0 up to now) has been done
-by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised
+by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised
 by C. Paulin. 
 
 An earlier implementation (versions 6.x) was due to B. Werner and
@@ -118,7 +118,7 @@ Axioms, and then "Extract Constant ..."
 
 
 [1]:
-Exécution de termes de preuves: une nouvelle méthode d'extraction 
+Exécution de termes de preuves: une nouvelle méthode d'extraction 
 pour le Calcul des Constructions Inductives, Pierre Letouzey,
 DEA thesis, 2000, 
 http://www.pps.jussieu.fr/~letouzey/download/rapport_dea.ps.gz
@@ -129,7 +129,7 @@ Types 2002 Post-Workshop Proceedings.
 http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz
 
 [3]: 
-Programmation fonctionnelle certifiée: l'extraction de programmes
+Programmation fonctionnelle certifiée: l'extraction de programmes
 dans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004.
 http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gz
 http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 626629063..9e257c82a 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Méthode d'élimination de Fourier *)
-(* Référence:
+(* Méthode d'élimination de Fourier *)
+(* Référence:
 Auteur(s) : Fourier, Jean-Baptiste-Joseph
 
-Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,...
+Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,...
 
-Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
+Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
 
 Pages: 326-327
 
@@ -20,8 +20,8 @@ http://gallica.bnf.fr/
 *)
 
 (* Un peu de calcul sur les rationnels...
-Les opérations rendent des rationnels normalisés,
-i.e. le numérateur et le dénominateur sont premiers entre eux.
+Les opérations rendent des rationnels normalisés,
+i.e. le numérateur et le dénominateur sont premiers entre eux.
 *)
 type rational = {num:int;
                  den:int}
@@ -59,9 +59,9 @@ let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
 let rinf x y = x.num*y.den < y.num*x.den;;
 let rinfeq x y = x.num*y.den <= y.num*x.den;;
 
-(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
+(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
 c1x1+...+cnxn < d si strict=true, <= sinon,
-hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
+hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
 *)
 
 type ineq = {coef:rational list;
@@ -70,8 +70,8 @@ type ineq = {coef:rational list;
 
 let pop x l = l:=x::(!l);;
 
-(* sépare la liste d'inéquations s selon que leur premier coefficient est
-négatif, nul ou positif. *)
+(* sépare la liste d'inéquations s selon que leur premier coefficient est
+négatif, nul ou positif. *)
 let partitionne s =
    let lpos=ref [] in
    let lneg=ref [] in
@@ -85,13 +85,13 @@ let partitionne s =
              s;
    [!lneg;!lnul;!lpos]
 ;;
-(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!):
-(add_hist [(equation 1, s1);...;(équation n, sn)])
+(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!):
+(add_hist [(equation 1, s1);...;(équation n, sn)])
 =
-[{équation 1, [1;0;...;0], s1};
- {équation 2, [0;1;...;0], s2};
+[{équation 1, [1;0;...;0], s1};
+ {équation 2, [0;1;...;0], s2};
  ...
- {équation n, [0;0;...;1], sn}]
+ {équation n, [0;0;...;1], sn}]
 *)
 let add_hist le =
    let n = List.length le in
@@ -105,24 +105,24 @@ let add_hist le =
               {coef=ie;hist=(!h);strict=s})
              le
 ;;
-(* additionne deux inéquations *)
+(* additionne deux inéquations *)
 let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef;
                       hist=List.map2 rplus ie1.hist ie2.hist;
 		      strict=ie1.strict || ie2.strict}
 ;;
-(* multiplication d'une inéquation par un rationnel (positif) *)
+(* multiplication d'une inéquation par un rationnel (positif) *)
 let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef;
                      hist=List.map (fun x -> rmult a x) ie.hist;
 		     strict= ie.strict}
 ;;
-(* on enlève le premier coefficient *)
+(* on enlève le premier coefficient *)
 let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict}
 ;;
-(* le premier coefficient: "tête" de l'inéquation *)
+(* le premier coefficient: "tête" de l'inéquation *)
 let hd_coef ie = List.hd ie.coef
 ;;
 
-(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient.
+(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient.
 *)
 let deduce_add lneg lpos =
    let res=ref [] in
@@ -136,8 +136,8 @@ let deduce_add lneg lpos =
              lneg;
    !res
 ;;
-(* élimination de la première variable à partir d'une liste d'inéquations:
-opération qu'on itère dans l'algorithme de Fourier.
+(* élimination de la première variable à partir d'une liste d'inéquations:
+opération qu'on itère dans l'algorithme de Fourier.
 *)
 let deduce1 s =
     match (partitionne s) with
@@ -146,7 +146,7 @@ let deduce1 s =
     (List.map ie_tl lnul)@lnew
      |_->assert false
 ;;
-(* algorithme de Fourier: on élimine successivement toutes les variables.
+(* algorithme de Fourier: on élimine successivement toutes les variables.
 *)
 let deduce lie =
    let n = List.length (fst (List.hd lie)) in
@@ -157,12 +157,12 @@ let deduce lie =
    !lie
 ;;
 
-(* donne [] si le système a des solutions,
+(* donne [] si le système a des solutions,
 sinon donne [c,s,lc]
-où lc est la combinaison linéaire des inéquations de départ
+où lc est la combinaison linéaire des inéquations de départ
 qui donne 0 < c si s=true
        ou 0 <= c sinon
-cette inéquation étant absurde.
+cette inéquation étant absurde.
 *)
 
 exception Contradiction of (rational * bool * rational list) list
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 4b70201b2..7274324d3 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -8,8 +8,8 @@
 
 
 
-(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
-des inéquations et équations sont entiers. En attendant la tactique Field.
+(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
+des inéquations et équations sont entiers. En attendant la tactique Field.
 *)
 
 open Term
@@ -22,10 +22,10 @@ open Fourier
 open Contradiction
 
 (******************************************************************************
-Opérations sur les combinaisons linéaires affines.
-La partie homogène d'une combinaison linéaire est en fait une table de hash
+Opérations sur les combinaisons linéaires affines.
+La partie homogène d'une combinaison linéaire est en fait une table de hash
 qui donne le coefficient d'un terme du calcul des constructions,
-qui est zéro si le terme n'y est pas.
+qui est zéro si le terme n'y est pas.
 *)
 
 module Constrhash = Hashtbl.Make
@@ -175,9 +175,9 @@ let flin_to_alist f =
     !res
 ;;
 
-(* Représentation des hypothèses qui sont des inéquations ou des équations.
+(* Représentation des hypothèses qui sont des inéquations ou des équations.
 *)
-type hineq={hname:constr; (* le nom de l'hypothèse *)
+type hineq={hname:constr; (* le nom de l'hypothèse *)
             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
             hleft:constr;
             hright:constr;
@@ -185,7 +185,7 @@ type hineq={hname:constr; (* le nom de l'hypothèse *)
             hstrict:bool}
 ;;
 
-(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
+(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 *)
 
 exception NoIneq
@@ -256,12 +256,12 @@ let ineq1_of_constr (h,t) =
       |_-> raise NoIneq
 ;;
 
-(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
+(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 *)
 
 let fourier_lineq lineq1 =
    let nvar=ref (-1) in
-   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
+   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
 		Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
 				nvar:=(!nvar)+1;
@@ -342,7 +342,7 @@ let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le")
 let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp")
 
 (******************************************************************************
-Construction de la preuve en cas de succès de la méthode de Fourier,
+Construction de la preuve en cas de succès de la méthode de Fourier,
 i.e. on obtient une contradiction.
 *)
 let is_int x = (x.den)=1
@@ -461,15 +461,15 @@ let mkAppL a =
 
 exception GoalDone
 
-(* Résolution d'inéquations linéaires dans R *)
+(* Résolution d'inéquations linéaires dans R *)
 let rec fourier () =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = strip_outer_cast concl in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
-    (* si le but est une inéquation, on introduit son contraire,
-       et le but à prouver devient False *)
+    (* si le but est une inéquation, on introduit son contraire,
+       et le but à prouver devient False *)
     try 
       match (kind_of_term goal) with
       App (f,args) ->
@@ -497,23 +497,23 @@ let rec fourier () =
 	    |_-> raise GoalDone)
         |_-> raise GoalDone
      with GoalDone ->
-    (* les hypothèses *)
+    (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (Proofview.Goal.hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 		        with NoIneq -> ())
               hyps;
-    (* lineq = les inéquations découlant des hypothèses *)
+    (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Errors.error "No inequalities";
     let res=fourier_lineq (!lineq) in
     let tac=ref (Proofview.tclUNIT ()) in
     if res=[]
     then Errors.error "fourier failed"
-    (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
+    (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
-    (* lc=coefficients multiplicateurs des inéquations
+    (* lc=coefficients multiplicateurs des inéquations
        qui donnent 0<cres ou 0<=cres selon sres *)
 	(*print_string "Fourier's method can prove the goal...";flush stdout;*)
           let lutil=ref [] in
@@ -523,7 +523,7 @@ let rec fourier () =
         		  then (lutil:=(h,c)::(!lutil)(*;
 				print_rational(c);print_string " "*)))
                     (List.combine (!lineq) lc);
-       (* on construit la combinaison linéaire des inéquation *)
+       (* on construit la combinaison linéaire des inéquation *)
              (match (!lutil) with
           (h1,c1)::lutil ->
 	  let s=ref (h1.hstrict) in
@@ -603,7 +603,7 @@ let rec fourier () =
 				    (mkApp (get coq_Rinv,
 				      [|get coq_R1|]))
 				    (get coq_R1))
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
+(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
       			        [Tacticals.New.tclORELSE
                                    (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 35699f219..cc89e2b9d 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -1,9 +1,9 @@
 (* ========================================================================= *)
 (* - This code originates from John Harrison's HOL LIGHT 2.30                *)
 (*   (see file LICENSE.sos for license, copyright and disclaimer)            *)
-(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL              *)
+(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL              *)
 (*   independent bits                                                        *)
-(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
+(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
 (* ========================================================================= *)
 
 (* ========================================================================= *)
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 235f9ce9b..f54914f25 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -2,9 +2,9 @@
 (* - This code originates from John Harrison's HOL LIGHT 2.30                *)
 (*   (see file LICENSE.sos for license, copyright and disclaimer)            *)
 (*   This code is the HOL LIGHT library code used by sos.ml                  *)
-(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL              *)
+(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL              *)
 (*   independent bits                                                        *)
-(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
+(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
 (* ========================================================================= *)
 
 open Num
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 8566cf0d6..464bc7740 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -602,7 +602,7 @@ and pgcd_pol_rec p q x =
 	    res
 	   )
 
-(* Sub-résultants:
+(* Sub-résultants:
 
    ai*Ai = Qi*Ai+1 + bi*Ai+2
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index b35ef1772..6d575a541 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -9,7 +9,7 @@
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
 (*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 83092ccc4..e425cff52 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -9,7 +9,7 @@
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
 (*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 4e9ca6ffc..efecc8add 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -9,7 +9,7 @@
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
 (*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
 (*                                                                        *)
 (* 13/10/2002 : modified to cope with an external numbering of equations  *)
 (*   and hypothesis. Its use for Omega is not more complex and it makes   *)
@@ -585,15 +585,6 @@ let rec depend relie_on accu = function
       end
   | [] -> relie_on, accu
 
-(*
-let depend relie_on accu trace =
-  Printf.printf "Longueur de la trace initiale : %d\n"
-    (trace_length trace + trace_length accu);
-  let rel',trace' = depend relie_on accu trace in
-  Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
-  rel',trace'
-*)
-
 let solve (new_eq_id,new_eq_var,print_var) system =
   try let _ = simplify new_eq_id false system in failwith "no contradiction"
   with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 3fa9e02cf..21b0f78b5 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -1,7 +1,7 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
+   Author: Pierre Crégut - France Télécom R&D
    Licence : LGPL version 2.1
 
  *************************************************************************)
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 4ae1cb94c..af50ea0ff 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -1,7 +1,7 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
+   Author: Pierre Crégut - France Télécom R&D
    Licence : LGPL version 2.1
 
  *************************************************************************)
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 4b6c9b790..0a99a26b3 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -1,7 +1,7 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
+   Author: Pierre Crégut - France Télécom R&D
    Licence : LGPL version 2.1
 
  *************************************************************************)
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index f9219407e..8156e8411 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1,7 +1,7 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
+   Author: Pierre Crégut - France Télécom R&D
    Licence : LGPL version 2.1
 
  *************************************************************************)
@@ -42,8 +42,8 @@ let occ_step_eq s1 s2 = match s1, s2 with
 | O_left, O_left | O_right, O_right | O_mono, O_mono -> true
 | _ -> false
 
-(* chemin identifiant une proposition sous forme du nom de l'hypothèse et
-   d'une liste de pas à partir de la racine de l'hypothèse *)
+(* chemin identifiant une proposition sous forme du nom de l'hypothèse et
+   d'une liste de pas à partir de la racine de l'hypothèse *)
 type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
 
 (* \subsection{refiable formulas} *)
@@ -63,7 +63,7 @@ type oformula =
 (* Operators for comparison recognized by Omega *)
 type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
 
-(* Type des prédicats réifiés (fragment de calcul propositionnel. Les
+(* Type des prédicats réifiés (fragment de calcul propositionnel. Les
  * quantifications sont externes au langage) *)
 type oproposition =
     Pequa of Term.constr * oequation
@@ -75,19 +75,19 @@ type oproposition =
   | Pimp of int * oproposition * oproposition
   | Pprop of Term.constr
 
-(* Les équations ou proposiitions atomiques utiles du calcul *)
+(* Les équations ou proposiitions atomiques utiles du calcul *)
 and oequation = {
     e_comp: comparaison;		(* comparaison *)
     e_left: oformula;			(* formule brute gauche *)
     e_right: oformula;			(* formule brute droite *)
     e_trace: Term.constr;		(* tactique de normalisation *)
-    e_origin: occurence;		(* l'hypothèse dont vient le terme *)
-    e_negated: bool;			(* vrai si apparait en position nié
-					   après normalisation *)
+    e_origin: occurence;		(* l'hypothèse dont vient le terme *)
+    e_negated: bool;			(* vrai si apparait en position nié
+					   après normalisation *)
     e_depends: direction  list;		(* liste des points de disjonction dont
-					   dépend l'accès à l'équation avec la
-					   direction (branche) pour y accéder *)
-    e_omega: afine		(* la fonction normalisée *)
+					   dépend l'accès à l'équation avec la
+					   direction (branche) pour y accéder *)
+    e_omega: afine		(* la fonction normalisée *)
   }
 
 (* \subsection{Proof context}
@@ -106,8 +106,8 @@ type environment = {
   mutable props : Term.constr list;
   (* Les variables introduites par omega *)
   mutable om_vars : (oformula * int) list;
-  (* Traduction des indices utilisés ici en les indices finaux utilisés par
-   * la tactique Omega après dénombrement des variables utiles *)
+  (* Traduction des indices utilisés ici en les indices finaux utilisés par
+   * la tactique Omega après dénombrement des variables utiles *)
   real_indices : (int,int) Hashtbl.t;
   mutable cnt_connectors : int;
   equations : (int,oequation) Hashtbl.t;
@@ -115,35 +115,35 @@ type environment = {
 }
 
 (* \subsection{Solution tree}
-   Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
-   d'un ensemble d'équation dont dépend la solution et d'une trace *)
-(* La liste des dépendances est triée et sans redondance *)
+   Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
+   d'un ensemble d'équation dont dépend la solution et d'une trace *)
+(* La liste des dépendances est triée et sans redondance *)
 type solution = {
   s_index : int;
   s_equa_deps : int list;
   s_trace : action list }
 
-(* Arbre de solution résolvant complètement un ensemble de systèmes *)
+(* Arbre de solution résolvant complètement un ensemble de systèmes *)
 type solution_tree =
     Leaf of solution
-    (* un noeud interne représente un point de branchement correspondant à
-       l'élimination d'un connecteur générant plusieurs buts
+    (* un noeud interne représente un point de branchement correspondant à
+       l'élimination d'un connecteur générant plusieurs buts
        (typ. disjonction). Le premier argument
        est l'identifiant du connecteur *)
   | Tree of int * solution_tree * solution_tree
 
-(* Représentation de l'environnement extrait du but initial sous forme de
-   chemins pour extraire des equations ou d'hypothèses *)
+(* Représentation de l'environnement extrait du but initial sous forme de
+   chemins pour extraire des equations ou d'hypothèses *)
 
 type context_content =
     CCHyp of occurence
   | CCEqua of int
 
 (* \section{Specific utility functions to handle base types} *)
-(* Nom arbitraire de l'hypothèse codant la négation du but final *)
+(* Nom arbitraire de l'hypothèse codant la négation du but final *)
 let id_concl = Names.Id.of_string "__goal__"
 
-(* Initialisation de l'environnement de réification de la tactique *)
+(* Initialisation de l'environnement de réification de la tactique *)
 let new_environment () = {
   terms = []; props = []; om_vars = []; cnt_connectors = 0;
   real_indices = Hashtbl.create 7;
@@ -151,17 +151,17 @@ let new_environment () = {
   constructors = Hashtbl.create 7;
 }
 
-(* Génération d'un nom d'équation *)
+(* Génération d'un nom d'équation *)
 let new_connector_id env =
    env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors
 
-(* Calcul de la branche complémentaire *)
+(* Calcul de la branche complémentaire *)
 let barre = function Left x -> Right x | Right x -> Left x
 
-(* Identifiant associé à une branche *)
+(* Identifiant associé à une branche *)
 let indice = function Left x | Right x -> x
 
-(* Affichage de l'environnement de réification (termes et propositions) *)
+(* Affichage de l'environnement de réification (termes et propositions) *)
 let print_env_reification env =
   let rec loop c i = function
       [] ->  str "  ===============================\n\n"
@@ -189,12 +189,12 @@ let new_omega_var, rst_omega_var =
   (function () -> incr cpt; !cpt),
   (function () -> cpt:=0)
 
-(* Affichage des variables d'un système *)
+(* Affichage des variables d'un système *)
 
 let display_omega_var i = Printf.sprintf "OV%d" i
 
-(* Recherche la variable codant un terme pour Omega et crée la variable dans
-   l'environnement si il n'existe pas. Cas ou la variable dans Omega représente
+(* Recherche la variable codant un terme pour Omega et crée la variable dans
+   l'environnement si il n'existe pas. Cas ou la variable dans Omega représente
    le terme d'un monome (le plus souvent un atome) *)
 
 let intern_omega env t =
@@ -204,22 +204,22 @@ let intern_omega env t =
     env.om_vars <- (t,v) :: env.om_vars; v
   end
 
-(* Ajout forcé d'un lien entre un terme et une variable  Cas où la
-   variable est créée par Omega et où il faut la lier après coup à un atome
-   réifié introduit de force *)
+(* Ajout forcé d'un lien entre un terme et une variable  Cas où la
+   variable est créée par Omega et où il faut la lier après coup à un atome
+   réifié introduit de force *)
 let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
 
-(* Récupère le terme associé à une variable *)
+(* Récupère le terme associé à une variable *)
 let unintern_omega env id =
   let rec loop = function
 	[] -> failwith "unintern"
       | ((t,j)::l) -> if Int.equal id j then t else loop l in
   loop env.om_vars
 
-(* \subsection{Gestion des environnements de variable pour la réflexion}
+(* \subsection{Gestion des environnements de variable pour la réflexion}
    Gestion des environnements de traduction entre termes des constructions
-   non réifiés et variables des termes reifies. Attention il s'agit de
-   l'environnement initial contenant tout. Il faudra le réduire après
+   non réifiés et variables des termes reifies. Attention il s'agit de
+   l'environnement initial contenant tout. Il faudra le réduire après
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
@@ -238,24 +238,24 @@ let add_prop env t =
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
-(* accès a une proposition *)
+(* accès a une proposition *)
 let get_prop v env =
   try List.nth v env with Invalid_argument _ -> failwith "get_prop"
 
-(* \subsection{Gestion du nommage des équations} *)
+(* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)
 let add_equation env e =
   let id = e.e_omega.id in
   try let _ = Hashtbl.find env.equations id in ()
   with Not_found -> Hashtbl.add env.equations id e
 
-(* accès a une equation *)
+(* accès a une equation *)
 let get_equation env id =
   try Hashtbl.find env.equations id
   with Not_found as e ->
-    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
+    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
-(* Affichage des termes réifiés *)
+(* Affichage des termes réifiés *)
 let rec oprint ch = function
   | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n)
   | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2
@@ -289,7 +289,7 @@ let rec weight env = function
   | Oufo _ -> -1
   | Oatom _ as c -> (intern_omega env c)
 
-(* \section{Passage entre oformules et représentation interne de Omega} *)
+(* \section{Passage entre oformules et représentation interne de Omega} *)
 
 (* \subsection{Oformula vers Omega} *)
 
@@ -332,12 +332,12 @@ let coq_of_formula env t =
   | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in
   loop t
 
-(* \subsection{Oformula vers COQ reifié} *)
+(* \subsection{Oformula vers COQ reifié} *)
 
 let reified_of_atom env i =
   try Hashtbl.find env.real_indices i
   with Not_found ->
-    Printf.printf "Atome %d non trouvé\n" i;
+    Printf.printf "Atome %d non trouvé\n" i;
     Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
     raise Not_found
 
@@ -390,7 +390,7 @@ let reified_of_proposition env f =
   try reified_of_proposition env f
   with reraise -> pprint stderr f; raise reraise
 
-(* \subsection{Omega vers COQ réifié} *)
+(* \subsection{Omega vers COQ réifié} *)
 
 let reified_of_omega env body constant =
   let coeff_constant =
@@ -407,13 +407,13 @@ let reified_of_omega env body c  =
   try reified_of_omega env body c
   with reraise -> display_eq display_omega_var (body,c); raise reraise
 
-(* \section{Opérations sur les équations}
-Ces fonctions préparent les traces utilisées par la tactique réfléchie
-pour faire des opérations de normalisation sur les équations.  *)
+(* \section{Opérations sur les équations}
+Ces fonctions préparent les traces utilisées par la tactique réfléchie
+pour faire des opérations de normalisation sur les équations.  *)
 
-(* \subsection{Extractions des variables d'une équation} *)
-(* Extraction des variables d'une équation. *)
-(* Chaque fonction retourne une liste triée sans redondance *)
+(* \subsection{Extractions des variables d'une équation} *)
+(* Extraction des variables d'une équation. *)
+(* Chaque fonction retourne une liste triée sans redondance *)
 
 let (@@) = List.merge_uniq compare
 
@@ -482,7 +482,7 @@ let rec negate = function
 
 let norm l = (List.length l)
 
-(* \subsection{Mélange (fusion) de deux équations} *)
+(* \subsection{Mélange (fusion) de deux équations} *)
 (* \subsubsection{Version avec coefficients} *)
 let shuffle_path k1 e1 k2 e2 =
   let rec loop = function
@@ -531,7 +531,7 @@ let rec shuffle env (t1,t2) =
 	do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1)
       else do_list [],Oplus(t1,t2)
 
-(* \subsection{Fusion avec réduction} *)
+(* \subsection{Fusion avec réduction} *)
 
 let shrink_pair f1 f2 =
   begin match f1,f2 with
@@ -563,7 +563,7 @@ let reduce_factor = function
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
   | t -> Errors.error "reduce_factor.1"
 
-(* \subsection{Réordonnancement} *)
+(* \subsection{Réordonnancement} *)
 
 let rec condense env = function
     Oplus(f1,(Oplus(f2,r) as t)) ->
@@ -596,7 +596,7 @@ let rec condense env = function
       let final = Oplus(t',Oint zero) in
       tac @ [Lazy.force coq_c_red6], final
 
-(* \subsection{Elimination des zéros} *)
+(* \subsection{Elimination des zéros} *)
 
 let rec clear_zero = function
    Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero ->
@@ -607,7 +607,7 @@ let rec clear_zero = function
       (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t)
   | t -> [],t;;
 
-(* \subsection{Transformation des hypothèses} *)
+(* \subsection{Transformation des hypothèses} *)
 
 let rec reduce env = function
     Oplus(t1,t2) ->
@@ -642,7 +642,7 @@ let normalize_linear_term env t =
   let trace3,t3 = clear_zero t2 in
   do_list [trace1; do_list trace2; do_list trace3], t3
 
-(* Cette fonction reproduit très exactement le comportement de [p_invert] *)
+(* Cette fonction reproduit très exactement le comportement de [p_invert] *)
 let negate_oper = function
     Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq
 
@@ -668,7 +668,7 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
 	  INEQ
   with e when Logic.catchable_exception e -> raise e
 
-(* \section{Compilation des hypothèses} *)
+(* \section{Compilation des hypothèses} *)
 
 let rec oformula_of_constr env t =
   match Z.parse_term t with
@@ -697,7 +697,7 @@ and binprop env (neg2,depends,origin,path)
     oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in
   let t2' =
     oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in
-  (* On numérote le connecteur dans l'environnement. *)
+  (* On numérote le connecteur dans l'environnement. *)
   c i t1' t2'
 
 and mk_equation env ctxt c connector t1 t2 =
@@ -736,7 +736,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
 	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
 
-(* Destructuration des hypothèses et de la conclusion *)
+(* Destructuration des hypothèses et de la conclusion *)
 
 let reify_gl env gl =
   let concl = Tacmach.pf_concl gl in
@@ -819,9 +819,9 @@ let destructurate_hyps syst =
     | [] -> [[]] in
   loop syst
 
-(* \subsection{Affichage d'un système d'équation} *)
+(* \subsection{Affichage d'un système d'équation} *)
 
-(* Affichage des dépendances de système *)
+(* Affichage des dépendances de système *)
 let display_depend = function
     Left i -> Printf.printf " L%d" i
   | Right i -> Printf.printf " R%d" i
@@ -852,8 +852,8 @@ let display_systems syst_list =
     List.iter display_equation syst in
   List.iter display_system syst_list
 
-(* Extraction des prédicats utilisées dans une trace. Permet ensuite le
-   calcul des hypothèses *)
+(* Extraction des prédicats utilisées dans une trace. Permet ensuite le
+   calcul des hypothèses *)
 
 let rec hyps_used_in_trace = function
   | act :: l ->
@@ -865,9 +865,9 @@ let rec hyps_used_in_trace = function
       end
   | [] -> []
 
-(* Extraction des variables déclarées dans une équation. Permet ensuite
-   de les déclarer dans l'environnement de la procédure réflexive et
-   éviter les créations de variable au vol *)
+(* Extraction des variables déclarées dans une équation. Permet ensuite
+   de les déclarer dans l'environnement de la procédure réflexive et
+   éviter les créations de variable au vol *)
 
 let rec variable_stated_in_trace = function
   | act :: l ->
@@ -885,7 +885,7 @@ let rec variable_stated_in_trace = function
 
 let add_stated_equations env tree =
   (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
-     de définir dans le mauvais ordre *)
+     de définir dans le mauvais ordre *)
   let stated_equations =
     let cmpvar x y = Pervasives.(-) x.st_var y.st_var in
     let rec loop = function
@@ -894,15 +894,15 @@ let add_stated_equations env tree =
     in loop tree
   in
   let add_env st =
-    (* On retransforme la définition de v en formule reifiée *)
+    (* On retransforme la définition de v en formule reifiée *)
     let v_def = oformula_of_omega env st.st_def in
-    (* Notez que si l'ordre de création des variables n'est pas respecté,
+    (* Notez que si l'ordre de création des variables n'est pas respecté,
      * ca va planter *)
     let coq_v = coq_of_formula env v_def in
     let v = add_reified_atom coq_v env in
     (* Le terme qu'il va falloir introduire *)
     let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in
-    (* sa représentation sous forme d'équation mais non réifié car on n'a pas
+    (* sa représentation sous forme d'équation mais non réifié car on n'a pas
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
     (* enregistre le lien entre la variable omega et la variable Coq *)
@@ -910,8 +910,8 @@ let add_stated_equations env tree =
     (v, term_to_generalize,term_to_reify,st.st_def.id) in
  List.map add_env stated_equations
 
-(* Calcule la liste des éclatements à réaliser sur les hypothèses
-   nécessaires pour extraire une liste d'équations donnée *)
+(* Calcule la liste des éclatements à réaliser sur les hypothèses
+   nécessaires pour extraire une liste d'équations donnée *)
 
 (* PL: experimentally, the result order of the following function seems
    _very_ crucial for efficiency. No idea why. Do not remove the List.rev
@@ -958,7 +958,7 @@ let really_useful_prop l_equa c =
     | Pnot t1 -> app coq_not [|real_of t1|]
     | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|]
     | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|]
-    (* Attention : implications sur le lifting des variables à comprendre ! *)
+    (* Attention : implications sur le lifting des variables à comprendre ! *)
     | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2)
     | Pprop t -> t in
   let rec loop c =
@@ -1166,11 +1166,11 @@ and decompose_tree_hyps trace env ctxt = function
 
 (* \section{La fonction principale} *)
  (* Cette fonction construit la
-trace pour la procédure de décision réflexive.  A partir des résultats
-de l'extraction des systèmes, elle lance la résolution par Omega, puis
+trace pour la procédure de décision réflexive.  A partir des résultats
+de l'extraction des systèmes, elle lance la résolution par Omega, puis
 l'extraction d'un ensemble minimal de solutions permettant la
-résolution globale du système et enfin construit la trace qui permet
-de faire rejouer cette solution par la tactique réflexive. *)
+résolution globale du système et enfin construit la trace qui permet
+de faire rejouer cette solution par la tactique réflexive. *)
 
 let resolution env full_reified_goal systems_list =
   let num = ref 0 in
@@ -1181,7 +1181,7 @@ let resolution env full_reified_goal systems_list =
       simplify_strong
 	(new_omega_eq,new_omega_var,display_omega_var)
 	system in
-    (* calcule les hypotheses utilisées pour la solution *)
+    (* calcule les hypotheses utilisées pour la solution *)
     let vars = hyps_used_in_trace trace in
     let splits = get_eclatement env vars in
     if !debug then begin
@@ -1202,7 +1202,7 @@ let resolution env full_reified_goal systems_list =
     display_solution_tree stdout solution_tree;
     print_newline()
   end;
-  (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *)
+  (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *)
   let useful_equa_id = equas_of_solution_tree solution_tree in
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
@@ -1225,8 +1225,8 @@ let resolution env full_reified_goal systems_list =
   let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
   let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
   (* L'environnement de base se construit en deux morceaux :
-     - les variables des équations utiles (et de la conclusion)
-     - les nouvelles variables declarées durant les preuves *)
+     - les variables des équations utiles (et de la conclusion)
+     - les nouvelles variables declarées durant les preuves *)
   let all_vars_env = useful_vars @ stated_vars in
   let basic_env =
     let rec loop i = function
@@ -1236,7 +1236,7 @@ let resolution env full_reified_goal systems_list =
       |	[] -> [] in
     loop 0 all_vars_env in
   let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
-  (* On peut maintenant généraliser le but : env est a jour *)
+  (* On peut maintenant généraliser le but : env est a jour *)
   let l_reified_stated =
      List.map (fun (_,_,(l,r),_) ->
                  app coq_p_eq [| reified_of_formula env l;