Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 88 insertions, 88 deletions

diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index c592af09a3..0fd92d6064 100644
--- a/plugins/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
@@ -12,17 +12,17 @@ Require Export Rbase.
 Comments "Lemmas used by the tactic Fourier".
 
 Open Scope R_scope.
- 
+
 Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1.
 intros; apply Rmult_lt_compat_l; assumption.
 Qed.
- 
+
 Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1.
 red in |- *.
 intros.
 case H; auto with real.
 Qed.
- 
+
 Lemma Rfourier_lt_lt :
  forall x1 y1 x2 y2 a:R,
    x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
@@ -33,7 +33,7 @@ apply Rfourier_lt.
 try exact H0.
 try exact H1.
 Qed.
- 
+
 Lemma Rfourier_lt_le :
  forall x1 y1 x2 y2 a:R,
    x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
@@ -48,7 +48,7 @@ rewrite (Rplus_comm x1 (a * y2)).
 apply Rplus_lt_compat_l.
 try exact H.
 Qed.
- 
+
 Lemma Rfourier_le_lt :
  forall x1 y1 x2 y2 a:R,
    x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
@@ -59,7 +59,7 @@ rewrite H2.
 apply Rplus_lt_compat_l.
 apply Rfourier_lt; auto with real.
 Qed.
- 
+
 Lemma Rfourier_le_le :
  forall x1 y1 x2 y2 a:R,
    x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2.
@@ -81,25 +81,25 @@ red in |- *.
 right; try assumption.
 auto with real.
 Qed.
- 
+
 Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
 intros x H; try assumption.
 rewrite Rplus_comm.
 apply Rle_lt_0_plus_1.
 red in |- *; auto with real.
 Qed.
- 
+
 Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
 intros x y H H0; try assumption.
 replace 0 with (x * 0).
 apply Rmult_lt_compat_l; auto with real.
 ring.
 Qed.
- 
+
 Lemma Rlt_zero_1 : 0 < 1.
 exact Rlt_0_1.
 Qed.
- 
+
 Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
 intros x H; try assumption.
 case H; intros.
@@ -112,7 +112,7 @@ red in |- *; left.
 exact Rlt_zero_1.
 ring.
 Qed.
- 
+
 Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
 intros x y H H0; try assumption.
 case H; intros.
@@ -121,12 +121,12 @@ apply Rlt_mult_inv_pos; auto with real.
 rewrite <- H1.
 red in |- *; right; ring.
 Qed.
- 
+
 Lemma Rle_zero_1 : 0 <= 1.
 red in |- *; left.
 exact Rlt_zero_1.
 Qed.
- 
+
 Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d.
 intros n d H; red in |- *; intros H0; try exact H0.
 generalize (Rgt_not_le 0 (n * / d)).
@@ -144,14 +144,14 @@ ring.
 ring.
 ring.
 Qed.
- 
+
 Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x.
 intros x; try assumption.
 replace (0 * x) with 0.
 apply Rlt_irrefl.
 ring.
 Qed.
- 
+
 Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d.
 intros n d H; try assumption.
 apply Rgt_not_le.
@@ -162,7 +162,7 @@ try exact H.
 ring.
 ring.
 Qed.
- 
+
 Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
 unfold not in |- *; intros.
 apply H.
@@ -173,7 +173,7 @@ try exact H0.
 ring.
 ring.
 Qed.
- 
+
 Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y.
 unfold not in |- *; intros.
 apply H.
@@ -188,35 +188,35 @@ ring.
 right.
 rewrite H1; ring.
 Qed.
- 
+
 Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y.
 unfold Rgt in |- *; intros; assumption.
 Qed.
- 
+
 Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y.
 intros x y; exact (Rge_le y x).
 Qed.
- 
+
 Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y.
 exact Req_le.
 Qed.
- 
+
 Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y.
 exact Req_le_sym.
 Qed.
- 
+
 Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y.
 exact Rnot_ge_lt.
 Qed.
- 
+
 Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y.
 exact Rnot_gt_le.
 Qed.
- 
+
 Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y.
 exact Rnot_le_lt.
 Qed.
- 
+
 Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y.
 exact Rnot_lt_ge.
 Qed.
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index dd54aea29a..73fb49295a 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -11,17 +11,17 @@
 (* 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,...
- 
+
 Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
- 
+
 Pages: 326-327
 
 http://gallica.bnf.fr/
 *)
 
-(* Un peu de calcul sur les rationnels... 
+(* 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.
 *)
@@ -45,7 +45,7 @@ let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
               else (let d=pgcd x.num x.den in
 		    let d= (if d<0 then -d else d) in
                     {num=(x.num)/d;den=(x.den)/d});;
- 
+
 let rop x = rnorm {num=(-x.num);den=x.den};;
 
 let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
@@ -72,7 +72,7 @@ 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 
+(* 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
@@ -98,7 +98,7 @@ let partitionne s =
 let add_hist le =
    let n = List.length le in
    let i=ref 0 in
-   List.map (fun (ie,s) -> 
+   List.map (fun (ie,s) ->
               let h =ref [] in
               for k=1 to (n-(!i)-1) do pop r0 h; done;
               pop r1 h;
@@ -107,7 +107,7 @@ 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}
@@ -142,7 +142,7 @@ let deduce_add lneg lpos =
 opération qu'on itère dans l'algorithme de Fourier.
 *)
 let deduce1 s =
-    match (partitionne s) with 
+    match (partitionne s) with
       [lneg;lnul;lpos] ->
     let lnew = deduce_add lneg lpos in
     (List.map ie_tl lnul)@lnew
@@ -172,7 +172,7 @@ let unsolvable lie =
    (try (List.iter (fun e ->
          match e with
            {coef=[c];hist=lc;strict=s} ->
-		  if (rinf c r0 && (not s)) || (rinfeq c r0 && s) 
+		  if (rinf c r0 && (not s)) || (rinfeq c r0 && s)
                   then (res := [c,s,lc];
 			raise (Failure "contradiction found"))
           |_->assert false)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 9082677008..3f490babd7 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -10,7 +10,7 @@
 
 
 
-(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients 
+(* 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.
 *)
 
@@ -26,9 +26,9 @@ 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 
-qui donne le coefficient d'un terme du calcul des constructions, 
-qui est zéro si le terme n'y est pas. 
+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.
 *)
 
 type flin = {fhom:(constr , rational)Hashtbl.t;
@@ -38,27 +38,27 @@ let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
 
 let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
 
-let flin_add f x c = 
+let flin_add f x c =
     let cx = flin_coef f x in
     Hashtbl.remove f.fhom x;
     Hashtbl.add f.fhom x (rplus cx c);
     f
 ;;
-let flin_add_cste f c = 
+let flin_add_cste f c =
     {fhom=f.fhom;
      fcste=rplus f.fcste c}
 ;;
 
 let flin_one () = flin_add_cste (flin_zero()) r1;;
 
-let flin_plus f1 f2 = 
+let flin_plus f1 f2 =
     let f3 = flin_zero() in
     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 ;;
 
-let flin_minus f1 f2 = 
+let flin_minus f1 f2 =
     let f3 = flin_zero() in
     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
@@ -69,17 +69,17 @@ let flin_emult a f =
     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
     flin_add_cste f2 (rmult a f.fcste);
 ;;
-    
+
 (*****************************************************************************)
 open Vernacexpr
 
 type ineq = Rlt | Rle | Rgt | Rge
 
-let string_of_R_constant kn = 
+let string_of_R_constant kn =
   match Names.repr_con kn with
-    | MPfile dir, sec_dir, id when 
-	sec_dir = empty_dirpath && 
-	string_of_dirpath dir = "Coq.Reals.Rdefinitions" 
+    | MPfile dir, sec_dir, id when
+	sec_dir = empty_dirpath &&
+	string_of_dirpath dir = "Coq.Reals.Rdefinitions"
 	-> string_of_label id
     | _ -> "constant_not_of_R"
 
@@ -94,20 +94,20 @@ let rec rational_of_constr c =
   | Cast (c,_,_) -> (rational_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
-	 | "Ropp" -> 
+	 | "Ropp" ->
 	     rop (rational_of_constr args.(0))
-	 | "Rinv" -> 
+	 | "Rinv" ->
 	     rinv (rational_of_constr args.(0))
-	 | "Rmult" -> 
+	 | "Rmult" ->
 	     rmult (rational_of_constr args.(0))
                    (rational_of_constr args.(1))
-	 | "Rdiv" -> 
+	 | "Rdiv" ->
 	     rdiv (rational_of_constr args.(0))
                   (rational_of_constr args.(1))
-	 | "Rplus" -> 
+	 | "Rplus" ->
 	     rplus (rational_of_constr args.(0))
                    (rational_of_constr args.(1))
-	 | "Rminus" -> 
+	 | "Rminus" ->
 	     rminus (rational_of_constr args.(0))
                     (rational_of_constr args.(1))
 	 | _ -> failwith "not a rational")
@@ -125,9 +125,9 @@ let rec flin_of_constr c =
   | Cast (c,_,_) -> (flin_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
-	   "Ropp" -> 
+	   "Ropp" ->
              flin_emult (rop r1) (flin_of_constr args.(0))
-	 | "Rplus"-> 
+	 | "Rplus"->
              flin_plus (flin_of_constr args.(0))
 	               (flin_of_constr args.(1))
 	 | "Rminus"->
@@ -138,10 +138,10 @@ let rec flin_of_constr c =
                      try (let b = (rational_of_constr args.(1)) in
 			    (flin_add_cste (flin_zero()) (rmult a b)))
 		     with _-> (flin_add (flin_zero())
-				 args.(1) 
+				 args.(1)
 				 a))
 	      with _-> (flin_add (flin_zero())
-			  args.(0) 
+			  args.(0)
 			  (rational_of_constr args.(1))))
 	 | "Rinv"->
 	     let a=(rational_of_constr args.(0)) in
@@ -151,7 +151,7 @@ let rec flin_of_constr c =
 		try (let a = (rational_of_constr args.(0)) in
 		       (flin_add_cste (flin_zero()) (rdiv a b)))
 		with _-> (flin_add (flin_zero())
-		            args.(0) 
+		            args.(0)
                             (rinv b)))
          |_->assert false)
   | Const c ->
@@ -254,19 +254,19 @@ let ineq1_of_constr (h,t) =
 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 *)
 
-let fourier_lineq lineq1 = 
+let fourier_lineq lineq1 =
    let nvar=ref (-1) in
    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
 		Hashtbl.iter (fun x _ -> if not (Hashtbl.mem hvar x) then begin
-				nvar:=(!nvar)+1; 
+				nvar:=(!nvar)+1;
 				Hashtbl.add hvar x (!nvar)
 			      end)
                   f.hflin.fhom)
              lineq1;
    let sys= List.map (fun h->
                let v=Array.create ((!nvar)+1) r0 in
-               Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) 
+               Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
                   h.hflin.fhom;
                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
              lineq1 in
@@ -346,7 +346,7 @@ let is_int x = (x.den)=1
 (* fraction = couple (num,den) *)
 let rec rational_to_fraction x= (x.num,x.den)
 ;;
-    
+
 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 *)
 let int_to_real n =
@@ -371,7 +371,7 @@ let rational_to_real x =
 let tac_zero_inf_pos gl (n,d) =
    let tacn=ref (apply (get coq_Rlt_zero_1)) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for i=1 to n-1 do 
+   for i=1 to n-1 do
        tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
    for i=1 to d-1 do
        tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
@@ -381,18 +381,18 @@ let tac_zero_inf_pos gl (n,d) =
 (* preuve que 0<=n*1/d
 *)
 let tac_zero_infeq_pos gl (n,d)=
-   let tacn=ref (if n=0 
+   let tacn=ref (if n=0
                  then (apply (get coq_Rle_zero_zero))
                  else (apply (get coq_Rle_zero_1))) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for i=1 to n-1 do 
+   for i=1 to n-1 do
        tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
    for i=1 to d-1 do
        tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
    (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
 ;;
-  
-(* preuve que 0<(-n)*(1/d) => False 
+
+(* preuve que 0<(-n)*(1/d) => False
 *)
 let tac_zero_inf_false gl (n,d) =
     if n=0 then (apply (get coq_Rnot_lt0))
@@ -401,7 +401,7 @@ let tac_zero_inf_false gl (n,d) =
 	      (tac_zero_infeq_pos gl (-n,d)))
 ;;
 
-(* preuve que 0<=(-n)*(1/d) => False 
+(* preuve que 0<=(-n)*(1/d) => False
 *)
 let tac_zero_infeq_false gl (n,d) =
      (tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
@@ -409,7 +409,7 @@ let tac_zero_infeq_false gl (n,d) =
 ;;
 
 let create_meta () = mkMeta(Evarutil.new_meta());;
-   
+
 let my_cut c gl=
      let concl = pf_concl gl in
        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
@@ -467,22 +467,22 @@ let rec fourier gl=
      match (kind_of_term goal) with
       App (f,args) ->
       (match (string_of_R_constr f) with
-	     "Rlt" -> 
+	     "Rlt" ->
 	       (tclTHEN
 	         (tclTHEN (apply (get coq_Rfourier_not_ge_lt))
 			  (intro_using  fhyp))
 		 fourier)
-	    |"Rle" -> 
+	    |"Rle" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_gt_le))
 		       (intro_using  fhyp))
 			fourier)
-	    |"Rgt" -> 
+	    |"Rgt" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_le_gt))
 		       (intro_using  fhyp))
 	      fourier)
-	    |"Rge" -> 
+	    |"Rge" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_lt_ge))
 		       (intro_using  fhyp))
@@ -490,7 +490,7 @@ let rec fourier gl=
 	    |_->assert false)
         |_->assert false
       in tac gl)
-     with _ -> 
+     with _ ->
     (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (pf_hyps gl)) in
@@ -511,12 +511,12 @@ let rec fourier gl=
        qui donnent 0<cres ou 0<=cres selon sres *)
 	(*print_string "Fourier's method can prove the goal...";flush stdout;*)
           let lutil=ref [] in
-	  List.iter 
+	  List.iter
             (fun (h,c) ->
 			  if c<>r0
         		  then (lutil:=(h,c)::(!lutil)(*;
 				print_rational(c);print_string " "*)))
-                    (List.combine (!lineq) lc); 
+                    (List.combine (!lineq) lc);
        (* on construit la combinaison linéaire des inéquation *)
              (match (!lutil) with
           (h1,c1)::lutil ->
@@ -545,7 +545,7 @@ let rec fourier gl=
 			      !t2 |] in
 	   let tc=rational_to_real cres in
        (* puis sa preuve *)
-           let tac1=ref (if h1.hstrict 
+           let tac1=ref (if h1.hstrict
                          then (tclTHENS (apply (get coq_Rfourier_lt))
                                  [tac_use h1;
                                   tac_zero_inf_pos  gl
@@ -555,24 +555,24 @@ let rec fourier gl=
 				  tac_zero_inf_pos  gl
                                       (rational_to_fraction c1)])) in
            s:=h1.hstrict;
-           List.iter (fun (h,c)-> 
+           List.iter (fun (h,c)->
              (if (!s)
 	      then (if h.hstrict
 	            then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt))
-			       [!tac1;tac_use h; 
+			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])
 	            else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le))
-			       [!tac1;tac_use h; 
+			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)]))
 	      else (if h.hstrict
 	            then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt))
-			       [!tac1;tac_use h; 
+			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])
 	            else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le))
-			       [!tac1;tac_use h; 
+			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])));
 	     s:=(!s)||(h.hstrict))
@@ -581,7 +581,7 @@ let rec fourier gl=
                       then tac_zero_inf_false gl (rational_to_fraction cres)
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
-           tac:=(tclTHENS (my_cut ineq) 
+           tac:=(tclTHENS (my_cut ineq)
                      [tclTHEN (change_in_concl None
 			       (mkAppL [| get coq_not; ineq|]
 				       ))
@@ -594,17 +594,17 @@ let rec fourier gl=
 		 	       [tac2;
                                 (tclTHENS
 				  (Equality.replace
-				    (mkApp (get coq_Rinv, 
+				    (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 ... *)
 
       			        [tclORELSE
                                    (Ring.polynom [])
                                    tclIDTAC;
 					  (tclTHEN (apply (get coq_sym_eqT))
 						(apply (get coq_Rinv_1)))]
-                               
+
 					 )
 				]));
                        !tac1]);
@@ -614,7 +614,7 @@ let rec fourier gl=
       |_-> assert false) |_-> assert false
 	  );
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
-      (!tac gl) 
+      (!tac gl)
 (*      ((tclABSTRACT None !tac) gl) *)
 
 ;;