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

9 files changed, 212 insertions, 212 deletions

diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v
index 47d67725f..bc7d73f62 100644
--- a/plugins/dp/Dp.v
+++ b/plugins/dp/Dp.v
@@ -103,14 +103,14 @@ Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
 Set Implicit Arguments.
 Section congr.
   Variable t:Type.
-Lemma ergo_eq_concat_1 : 
+Lemma ergo_eq_concat_1 :
   forall (P:t -> Prop) (x y:t),
     P x -> x = y -> P y.
 Proof.
   intros; subst; auto.
 Qed.
 
-Lemma ergo_eq_concat_2 : 
+Lemma ergo_eq_concat_2 :
   forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
     P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
 Proof.
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index a7e1a8206..dc4698c5e 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -1,7 +1,7 @@
 (* Authors: Nicolas Ayache and Jean-Christophe Filliâtre *)
 (* Tactics to call decision procedures *)
 
-(* Works in two steps: 
+(* Works in two steps:
 
    - first the Coq context and the current goal are translated in
      Polymorphic First-Order Logic (see fol.mli in this directory)
@@ -36,27 +36,27 @@ let set_trace b = trace := b
 let timeout = ref 10
 let set_timeout n = timeout := n
 
-let (dp_timeout_obj,_) = 
-  declare_object 
-    {(default_object "Dp_timeout") with  
+let (dp_timeout_obj,_) =
+  declare_object
+    {(default_object "Dp_timeout") with
        cache_function = (fun (_,x) -> set_timeout x);
        load_function = (fun _ (_,x) -> set_timeout x);
        export_function = (fun x -> Some x)}
 
 let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
 
-let (dp_debug_obj,_) = 
-  declare_object 
-    {(default_object "Dp_debug") with  
+let (dp_debug_obj,_) =
+  declare_object
+    {(default_object "Dp_debug") with
        cache_function = (fun (_,x) -> set_debug x);
        load_function = (fun _ (_,x) -> set_debug x);
        export_function = (fun x -> Some x)}
 
 let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
 
-let (dp_trace_obj,_) = 
-  declare_object 
-    {(default_object "Dp_trace") with  
+let (dp_trace_obj,_) =
+  declare_object
+    {(default_object "Dp_trace") with
        cache_function = (fun (_,x) -> set_trace x);
        load_function = (fun _ (_,x) -> set_trace x);
        export_function = (fun x -> Some x)}
@@ -67,7 +67,7 @@ let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
   init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
     @ [["Coq"; "ZArith"; "BinInt"];
-       ["Coq"; "Reals"; "Rdefinitions"]; 
+       ["Coq"; "Reals"; "Rdefinitions"];
        ["Coq"; "Reals"; "Raxioms";];
        ["Coq"; "Reals"; "Rbasic_fun";];
        ["Coq"; "Reals"; "R_sqrt";];
@@ -123,36 +123,36 @@ let global_names = Hashtbl.create 97
 let used_names = Hashtbl.create 97
 
 let rename_global r =
-  try 
+  try
     Hashtbl.find global_names r
   with Not_found ->
-    let rec loop id = 
-      if Hashtbl.mem used_names id then 
+    let rec loop id =
+      if Hashtbl.mem used_names id then
 	loop (lift_ident id)
-      else begin 
+      else begin
 	Hashtbl.add used_names id ();
 	let s = string_of_id id in
-	Hashtbl.add global_names r s; 
+	Hashtbl.add global_names r s;
 	s
       end
     in
     loop (Nametab.basename_of_global r)
 
 let foralls =
-  List.fold_right 
+  List.fold_right
     (fun (x,t) p -> Forall (x, t, p))
 
 let fresh_var = function
   | Anonymous -> rename_global (VarRef (id_of_string "x"))
   | Name x -> rename_global (VarRef x)
 
-(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of 
-   env names, and returns the new variables together with the new 
+(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
+   env names, and returns the new variables together with the new
    environment *)
 let coq_rename_vars env vars =
   let avoid = ref (ids_of_named_context (Environ.named_context env)) in
   List.fold_right
-    (fun (na,t) (newvars, newenv) -> 
+    (fun (na,t) (newvars, newenv) ->
        let id = next_name_away na !avoid in
        avoid := id :: !avoid;
        id :: newvars, Environ.push_named (id, None, t) newenv)
@@ -162,9 +162,9 @@ let coq_rename_vars env vars =
    type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
 let decomp_type_quantifiers env t =
   let rec loop vars t = match kind_of_term t with
-    | Prod (n, a, t) when is_Set a || is_Type a -> 
+    | Prod (n, a, t) when is_Set a || is_Type a ->
 	loop ((n,a) :: vars) t
-    | _ -> 
+    | _ ->
 	let vars, env = coq_rename_vars env vars in
 	let t = substl (List.map mkVar vars) t in
 	List.rev vars, env, t
@@ -174,21 +174,21 @@ let decomp_type_quantifiers env t =
 (* same thing with lambda binders (for axiomatize body) *)
 let decomp_type_lambdas env t =
   let rec loop vars t = match kind_of_term t with
-    | Lambda (n, a, t) when is_Set a || is_Type a -> 
+    | Lambda (n, a, t) when is_Set a || is_Type a ->
 	loop ((n,a) :: vars) t
-    | _ -> 
+    | _ ->
 	let vars, env = coq_rename_vars env vars in
 	let t = substl (List.map mkVar vars) t in
 	List.rev vars, env, t
   in
   loop [] t
 
-let decompose_arrows = 
+let decompose_arrows =
   let rec arrows_rec l c = match kind_of_term c with
     | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
     | Cast (c,_,_) -> arrows_rec l c
     | _ -> List.rev l, c
-  in 
+  in
   arrows_rec []
 
 let rec eta_expanse t vars env i =
@@ -203,7 +203,7 @@ let rec eta_expanse t vars env i =
 	  let env' = Environ.push_named (id, None, a) env in
 	  let t' = mkApp (t, [| mkVar id |]) in
 	  eta_expanse t' (id :: vars) env' (pred i)
-      | _ -> 
+      | _ ->
 	  assert false
 
 let rec skip_k_args k cl = match k, cl with
@@ -222,7 +222,7 @@ let globals_stack = ref []
 let () =
   Summary.declare_summary "Dp globals"
     { Summary.freeze_function = (fun () -> !globals, !globals_stack);
-      Summary.unfreeze_function = 
+      Summary.unfreeze_function =
 	(fun (g,s) -> globals := g; globals_stack := s);
       Summary.init_function = (fun () -> ()) }
 
@@ -238,7 +238,7 @@ let lookup_local r =  match Hashtbl.find locals r with
   | Gnot_fo -> raise NotFO
   | Gfo d -> d
 
-let iter_all_constructors i f =  
+let iter_all_constructors i f =
   let _, oib = Global.lookup_inductive i in
   Array.iteri
     (fun j tj -> f j (mkConstruct (i, j+1)))
@@ -246,7 +246,7 @@ let iter_all_constructors i f =
 
 
 (* injection c [t1,...,tn] adds the injection axiom
-     forall x1:t1,...,xn:tn,y1:t1,...,yn:tn. 
+     forall x1:t1,...,xn:tn,y1:t1,...,yn:tn.
        c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *)
 
 let injection c l =
@@ -255,8 +255,8 @@ let injection c l =
   let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in
   i := 0;
   let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in
-  let f = 
-    List.fold_right2 
+  let f =
+    List.fold_right2
       (fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p))
       xl yl True
   in
@@ -267,14 +267,14 @@ let injection c l =
   let ax = Axiom ("injection_" ^ c, f) in
   globals_stack := ax :: !globals_stack
 
-(* rec_names_for c [|n1;...;nk|] builds the list of constant names for 
+(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
    identifiers n1...nk with the same path as c, if they exist; otherwise
    raises Not_found *)
 let rec_names_for c =
   let mp,dp,_ = Names.repr_con c in
   array_map_to_list
-    (function 
-       | Name id -> 
+    (function
+       | Name id ->
 	   let c' = Names.make_con mp dp (label_of_id id) in
 	   ignore (Global.lookup_constant c');
 	   msgnl (Printer.pr_constr (mkConst c'));
@@ -286,7 +286,7 @@ let rec_names_for c =
 
 let term_abstractions = Hashtbl.create 97
 
-let new_abstraction = 
+let new_abstraction =
   let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r
 
 (* Arithmetic constants *)
@@ -345,14 +345,14 @@ let rec tr_arith_constant t = match kind_of_term t with
       tr_powerRZ a b
   | Term.Cast (t, _, _) ->
       tr_arith_constant t
-  | _ -> 
+  | _ ->
       raise NotArithConstant
 
 (* translates a constant of the form (powerRZ 2 int_constant) *)
 and tr_powerRZ a b =
   (* checking first that a is (R1 + R1) *)
   match kind_of_term a with
-  | Term.App (f, [|c;d|]) when f = Lazy.force coq_Rplus -> 
+  | Term.App (f, [|c;d|]) when f = Lazy.force coq_Rplus ->
       begin
       match kind_of_term c,kind_of_term d with
         | Term.Const _, Term.Const _
@@ -371,9 +371,9 @@ and tr_powerRZ a b =
    tv = list of type variables *)
 and tr_type tv env t =
   let t = Reductionops.nf_betadeltaiota env Evd.empty t in
-  if t = Lazy.force coq_Z then 
+  if t = Lazy.force coq_Z then
     Tid ("int", [])
-  else if t = Lazy.force coq_R then 
+  else if t = Lazy.force coq_R then
     Tid ("real", [])
   else match kind_of_term t with
     | Var x when List.mem x tv ->
@@ -383,15 +383,15 @@ and tr_type tv env t =
 	begin try
 	  let r = global_of_constr f in
 	  match tr_global env r with
-	    | DeclType (id, k) -> 
+	    | DeclType (id, k) ->
 		assert (k = List.length cl); (* since t:Set *)
 		Tid (id, List.map (tr_type tv env) cl)
-	    | _ -> 
+	    | _ ->
 		raise NotFO
-	with 
+	with
 	  | Not_found ->
 	      raise NotFO
-	  | NotFO -> 
+	  | NotFO ->
 	      (* we need to abstract some part of (f cl) *)
 	      (*TODO*)
 	      raise NotFO
@@ -403,8 +403,8 @@ and make_term_abstraction tv env c =
   match tr_decl env id ty with
     | DeclFun (id,_,_,_) as _d ->
         raise NotFO
-        (* [CM 07/09/2009] deactivated because it generates 
-           unbound identifiers 'abstraction_<number>' 
+        (* [CM 07/09/2009] deactivated because it generates
+           unbound identifiers 'abstraction_<number>'
 	begin try
 	  Hashtbl.find term_abstractions c
 	with Not_found ->
@@ -428,7 +428,7 @@ and tr_decl env id ty =
     DeclType (id, List.length tv)
   else if is_Prop t then
     DeclPred (id, List.length tv, [])
-  else 
+  else
     let s = Typing.type_of env Evd.empty t in
     if is_Prop s then
       Axiom (id, tr_formula tv [] env t)
@@ -437,11 +437,11 @@ and tr_decl env id ty =
       let l = List.map (tr_type tv env) l in
       if is_Prop t then
 	DeclPred(id, List.length tv, l)
-      else 
+      else
 	let s = Typing.type_of env Evd.empty t in
-	if is_Set s || is_Type s then 
+	if is_Set s || is_Type s then
 	  DeclFun (id, List.length tv, l, tr_type tv env t)
-	else 
+	else
 	  raise NotFO
 
 (* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *)
@@ -457,7 +457,7 @@ and tr_global env r = match r with
 	  let id = rename_global r in
 	  let d = tr_decl env id ty in
 	  (* r can be already declared if it is a constructor *)
-	  if not (mem_global r) then begin 
+	  if not (mem_global r) then begin
 	    add_global r (Gfo d);
 	    globals_stack := d :: !globals_stack
 	  end;
@@ -468,7 +468,7 @@ and tr_global env r = match r with
 	  raise NotFO
 
 and axiomatize_body env r id d = match r with
-  | VarRef _ -> 
+  | VarRef _ ->
       assert false
   | ConstRef c ->
       begin match (Global.lookup_constant c).const_body with
@@ -488,7 +488,7 @@ and axiomatize_body env r id d = match r with
 		     (*Format.eprintf "axiomatize_body %S@." id;*)
 		     let b = match kind_of_term b with
 		       (* a single recursive function *)
-		       | Fix (_, (_,_,[|b|])) -> 
+		       | Fix (_, (_,_,[|b|])) ->
 			   subst1 (mkConst c) b
                        (* mutually recursive functions *)
 		       | Fix ((_,i), (names,_,bodies)) ->
@@ -499,7 +499,7 @@ and axiomatize_body env r id d = match r with
 			   with Not_found ->
 			     b
 			   end
-		       | _ -> 
+		       | _ ->
 			   b
 		     in
 		     let tv, env, b = decomp_type_lambdas env b in
@@ -521,9 +521,9 @@ and axiomatize_body env r id d = match r with
 			   begin match kind_of_term t with
 			     | Case (ci, _, e, br) ->
 				 equations_for_case env id vars tv bv ci e br
-			     | _ -> 
+			     | _ ->
 				 let t = tr_term tv bv env t in
-				 let ax = 
+				 let ax =
 				   add_proof (Fun_def (id, vars, ty, t))
 				 in
 				 let p = Fatom (Eq (App (id, fol_vars), t)) in
@@ -542,7 +542,7 @@ and axiomatize_body env r id d = match r with
 	    in
 	    let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in
 	    globals_stack := axioms @ !globals_stack
-	| None -> 
+	| None ->
 	    () (* Coq axiom *)
       end
   | IndRef i ->
@@ -597,12 +597,12 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
 		     | (y, t)::l' -> if y = string_of_id e then l'
 		       else (y, t)::(remove l' e) in
 		   let vars = remove vars x in
-		   let p = 
-		     Fatom (Eq (App (id, fol_vars), 
+		   let p =
+		     Fatom (Eq (App (id, fol_vars),
 				tr_term tv bv env b))
 		   in
 		   eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs
-	       | _ -> 
+	       | _ ->
 		   assert false end
 	   with NotFO ->
 	     ());
@@ -611,30 +611,30 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
       raise NotFO
 
 (* assumption: t:T:Set *)
-and tr_term tv bv env t = 
+and tr_term tv bv env t =
       try
 	tr_arith_constant t
       with NotArithConstant ->
   match kind_of_term t with
     (* binary operations on integers *)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus ->
       Plus (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus ->
       Moins (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult ->
       Mult (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv ->
       Div (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zopp -> 
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zopp ->
       Opp (tr_term tv bv env a)
     (* binary operations on reals *)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus ->
       Plus (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rminus -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rminus ->
       Moins (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult ->
       Mult (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rdiv -> 
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rdiv ->
       Div (tr_term tv bv env a, tr_term tv bv env b)
   | Term.Var id when List.mem id bv ->
       App (string_of_id id, [])
@@ -643,12 +643,12 @@ and tr_term tv bv env t =
 	begin try
 	  let r = global_of_constr f in
 	  match tr_global env r with
-	    | DeclFun (s, k, _, _) -> 
+	    | DeclFun (s, k, _, _) ->
 		let cl = skip_k_args k cl in
 		Fol.App (s, List.map (tr_term tv bv env) cl)
-	    | _ -> 
+	    | _ ->
 		raise NotFO
-	with 
+	with
 	  | Not_found ->
 	      raise NotFO
 	  | NotFO -> (* we need to abstract some part of (f cl) *)
@@ -663,7 +663,7 @@ and tr_term tv bv env t =
 		      abstract (applist (app, [x])) l
 		    end
 	      in
-	      let app,l = match cl with 
+	      let app,l = match cl with
 		| x :: l -> applist (f, [x]), l | [] -> raise NotFO
 	      in
 	      abstract app l
@@ -681,14 +681,14 @@ and quantifiers n a b tv bv env =
 and tr_formula tv bv env f =
   let c, args = decompose_app f in
   match kind_of_term c, args with
-    | Var id, [] -> 
+    | Var id, [] ->
 	Fatom (Pred (rename_global (VarRef id), []))
     | _, [t;a;b] when c = build_coq_eq () ->
 	let ty = Typing.type_of env Evd.empty t in
 	if is_Set ty || is_Type ty then
 	  let _ = tr_type tv env t in
 	  Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
-	else 
+	else
 	  raise NotFO
           (* comparisons on integers *)
     | _, [a;b] when c = Lazy.force coq_Zle ->
@@ -731,7 +731,7 @@ and tr_formula tv bv env f =
 	  | Lambda(n, a, b) ->
 	      let id, t, bv, env, b = quantifiers n a b tv bv env in
 	      Exists (string_of_id id, t, tr_formula tv bv env b)
-	  | _ -> 
+	  | _ ->
 	      (* unusual case of the shape (ex p) *)
 	      raise NotFO (* TODO: we could eta-expanse *)
 	end
@@ -739,10 +739,10 @@ and tr_formula tv bv env f =
 	begin try
 	  let r = global_of_constr c in
 	  match tr_global env r with
-	    | DeclPred (s, k, _) -> 
+	    | DeclPred (s, k, _) ->
 		let args = skip_k_args k args in
 		Fatom (Pred (s, List.map (tr_term tv bv env) args))
-	    | _ -> 
+	    | _ ->
 		raise NotFO
 	with Not_found ->
 	  raise NotFO
@@ -751,7 +751,7 @@ and tr_formula tv bv env f =
 
 let tr_goal gl =
   Hashtbl.clear locals;
-  let tr_one_hyp (id, ty) = 
+  let tr_one_hyp (id, ty) =
     try
       let s = rename_global (VarRef id) in
       let d = tr_decl (pf_env gl) s ty in
@@ -762,7 +762,7 @@ let tr_goal gl =
       raise NotFO
   in
   let hyps =
-    List.fold_right 
+    List.fold_right
       (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
       (pf_hyps_types gl) []
   in
@@ -781,9 +781,9 @@ let file_contents f =
   let buf = Buffer.create 1024 in
   try
     let c = open_in f in
-    begin try 
-      while true do 
-	let s = input_line c in Buffer.add_string buf s; 
+    begin try
+      while true do
+	let s = input_line c in Buffer.add_string buf s;
 	Buffer.add_char buf '\n'
       done;
       assert false
@@ -791,7 +791,7 @@ let file_contents f =
       close_in c;
       Buffer.contents buf
     end
-  with _ -> 
+  with _ ->
     sprintf "(cannot open %s)" f
 
 let timeout_sys_command cmd =
@@ -799,24 +799,24 @@ let timeout_sys_command cmd =
   let out = Filename.temp_file "out" "" in
   let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
   let ret = Sys.command cmd in
-  if !debug then 
+  if !debug then
     Format.eprintf "Output file %s:@.%s@." out (file_contents out);
   ret, out
 
 let timeout_or_failure c cmd out =
-  if c = 152 then 
-    Timeout 
+  if c = 152 then
+    Timeout
   else
-    Failure 
+    Failure
       (sprintf "command %s failed with output:\n%s " cmd (file_contents out))
 
 let prelude_files = ref ([] : string list)
 
 let set_prelude l = prelude_files := l
 
-let (dp_prelude_obj,_) = 
-  declare_object 
-    {(default_object "Dp_prelude") with  
+let (dp_prelude_obj,_) =
+  declare_object
+    {(default_object "Dp_prelude") with
        cache_function = (fun (_,x) -> set_prelude x);
        load_function = (fun _ (_,x) -> set_prelude x);
        export_function = (fun x -> Some x)}
@@ -826,18 +826,18 @@ let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
 let why_files f = String.concat " " (!prelude_files @ [f])
 
 let call_simplify fwhy =
-  let cmd = 
-    sprintf "why --simplify %s" (why_files fwhy) 
+  let cmd =
+    sprintf "why --simplify %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
-  let cmd = 
-    sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out" 
+  let cmd =
+    sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
       !timeout fsx
   in
   let out = Sys.command cmd in
-  let r = 
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  let r =
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
   in
   if not !debug then remove_files [fwhy; fsx];
   r
@@ -847,15 +847,15 @@ let call_ergo fwhy =
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
   let ftrace = Filename.temp_file "ergo_trace" "" in
-  let cmd = 
+  let cmd =
     if !trace then
       sprintf "alt-ergo -cctrace %s %s" ftrace fwhy
     else
       sprintf "alt-ergo %s" fwhy
   in
   let ret,out = timeout_sys_command cmd in
-  let r = 
-    if ret <> 0 then 
+  let r =
+    if ret <> 0 then
       timeout_or_failure ret cmd out
     else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
       Valid (if !trace then Some ftrace else None)
@@ -871,18 +871,18 @@ let call_ergo fwhy =
 
 
 let call_zenon fwhy =
-  let cmd = 
+  let cmd =
     sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
   let out = Filename.temp_file "dp_out" "" in
-  let cmd = 
-    sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out 
+  let cmd =
+    sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
   in
   let c = Sys.command cmd in
   if not !debug then remove_files [fwhy; fznn];
-  if c = 137 then 
+  if c = 137 then
     Timeout
   else begin
     if c <> 0 then anomaly ("command failed: " ^ cmd);
@@ -893,58 +893,58 @@ let call_zenon fwhy =
   end
 
 let call_yices fwhy =
-  let cmd = 
+  let cmd =
     sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
-  let cmd = 
-    sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out" 
+  let cmd =
+    sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
       !timeout fsmt
   in
   let out = Sys.command cmd in
-  let r = 
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  let r =
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
   in
   if not !debug then remove_files [fwhy; fsmt];
   r
 
 let call_cvc3 fwhy =
-  let cmd = 
+  let cmd =
     sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
-  let cmd = 
-    sprintf "why-cpulimit %d cvc3 -lang smt %s > out 2>&1 && grep -q -w unsat out" 
+  let cmd =
+    sprintf "why-cpulimit %d cvc3 -lang smt %s > out 2>&1 && grep -q -w unsat out"
       !timeout fsmt
   in
   let out = Sys.command cmd in
-  let r = 
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  let r =
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
   in
   if not !debug then remove_files [fwhy; fsmt];
   r
 
 let call_cvcl fwhy =
-  let cmd = 
+  let cmd =
     sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
-  let cmd = 
-    sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out" 
+  let cmd =
+    sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
       !timeout fcvc
   in
   let out = Sys.command cmd in
-  let r = 
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  let r =
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
   in
   if not !debug then remove_files [fwhy; fcvc];
   r
 
 let call_harvey fwhy =
-  let cmd = 
+  let cmd =
     sprintf "why --harvey --encoding strat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
@@ -953,15 +953,15 @@ let call_harvey fwhy =
   if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed");
   let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
   let outf = Filename.temp_file "rv" ".out" in
-  let out = 
-    Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1" 
-		   !timeout f outf) 
+  let out =
+    Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
+		   !timeout f outf)
   in
   let r =
-    if out <> 0 then 
+    if out <> 0 then
       Timeout
     else
-      let cmd = 
+      let cmd =
 	sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
       in
       if Sys.command cmd = 0 then Valid None else Invalid
@@ -1000,12 +1000,12 @@ let call_prover prover q =
     | CVCLite -> call_cvcl fwhy
     | Harvey -> call_harvey fwhy
     | Gwhy -> call_gwhy fwhy
-  
+
 let dp prover gl =
   Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
   let concl_type = pf_type_of gl (pf_concl gl) in
   if not (is_Prop concl_type) then error "Conclusion is not a Prop";
-  try 
+  try
     let q = tr_goal gl in
     begin match call_prover prover q with
       | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
@@ -1019,7 +1019,7 @@ let dp prover gl =
     end
   with NotFO ->
     error "Not a first order goal"
-      
+
 
 let simplify = tclTHEN intros (dp Simplify)
 let ergo = tclTHEN intros (dp Ergo)
@@ -1032,7 +1032,7 @@ let gwhy = tclTHEN intros (dp Gwhy)
 
 let dp_hint l =
   let env = Global.env () in
-  let one_hint (qid,r) = 
+  let one_hint (qid,r) =
     if not (mem_global r) then begin
       let ty = Global.type_of_global r in
       let s = Typing.type_of env Evd.empty ty in
@@ -1046,7 +1046,7 @@ let dp_hint l =
 	with NotFO ->
 	  add_global r Gnot_fo;
 	  msg_warning
-	    (pr_reference qid ++ 
+	    (pr_reference qid ++
 	     str " ignored (not a first order proposition)")
 	else begin
 	  add_global r Gnot_fo;
@@ -1057,9 +1057,9 @@ let dp_hint l =
   in
   List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
 
-let (dp_hint_obj,_) = 
-  declare_object 
-    {(default_object "Dp_hint") with  
+let (dp_hint_obj,_) =
+  declare_object
+    {(default_object "Dp_hint") with
        cache_function = (fun (_,l) -> dp_hint l);
        load_function = (fun _ (_,l) -> dp_hint l);
        export_function = (fun x -> Some x)}
@@ -1075,7 +1075,7 @@ let dp_predefined qid s =
     let d = match tr_decl env id ty with
       | DeclType (_, n) -> DeclType (s, n)
       | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
-      | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl) 
+      | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
       | Axiom _ as d -> d
     in
     match d with
@@ -1084,22 +1084,22 @@ let dp_predefined qid s =
   with NotFO ->
     msg_warning (str " ignored (not a first order declaration)")
 
-let (dp_predefined_obj,_) = 
-  declare_object 
-    {(default_object "Dp_predefined") with  
+let (dp_predefined_obj,_) =
+  declare_object
+    {(default_object "Dp_predefined") with
        cache_function = (fun (_,(id,s)) -> dp_predefined id s);
        load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
        export_function = (fun x -> Some x)}
 
 let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
 
-let _ = declare_summary "Dp options" 
-	  { freeze_function = 
+let _ = declare_summary "Dp options"
+	  { freeze_function =
 	      (fun () -> !debug, !trace, !timeout, !prelude_files);
-	    unfreeze_function = 
-	      (fun (d,tr,tm,pr) -> 
+	    unfreeze_function =
+	      (fun (d,tr,tm,pr) ->
 		debug := d; trace := tr; timeout := tm; prelude_files := pr);
-	    init_function = 
-	      (fun () -> 
-		debug := false; trace := false; timeout := 10; 
-		prelude_files := []) }  
+	    init_function =
+	      (fun () ->
+		debug := false; trace := false; timeout := 10;
+		prelude_files := []) }
diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml
index 94dc0ef48..4a1d70d41 100644
--- a/plugins/dp/dp_why.ml
+++ b/plugins/dp/dp_why.ml
@@ -4,12 +4,12 @@
 open Format
 open Fol
 
-type proof = 
+type proof =
   | Immediate of Term.constr
   | Fun_def of string * (string * typ) list * typ * term
 
 let proofs = Hashtbl.create 97
-let proof_name = 
+let proof_name =
   let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r
 
 let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n
@@ -24,9 +24,9 @@ let rec print_list sep print fmt = function
 let space fmt () = fprintf fmt "@ "
 let comma fmt () = fprintf fmt ",@ "
 
-let is_why_keyword = 
+let is_why_keyword =
   let h = Hashtbl.create 17 in
-  List.iter 
+  List.iter
     (fun s -> Hashtbl.add h s ())
     ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin";
      "bool"; "do"; "done"; "else"; "end"; "exception"; "exists";
@@ -34,7 +34,7 @@ let is_why_keyword =
      "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not";
      "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises";
      "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try";
-     "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; 
+     "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ];
   Hashtbl.mem h
 
 let ident fmt s =
@@ -49,9 +49,9 @@ let rec print_typ fmt = function
   | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x
 
 let rec print_term fmt = function
-  | Cst n -> 
+  | Cst n ->
       fprintf fmt "%s" (Big_int.string_of_big_int n)
-  | RCst s -> 
+  | RCst s ->
       fprintf fmt "%s.0" (Big_int.string_of_big_int s)
   | Power2 n ->
       fprintf fmt "0x1p%s" (Big_int.string_of_big_int n)
@@ -64,17 +64,17 @@ let rec print_term fmt = function
   | Div (a, b) ->
       fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b
   | Opp (a) ->
-      fprintf fmt "@[(-@ %a)@]" print_term a 
+      fprintf fmt "@[(-@ %a)@]" print_term a
   | App (id, []) ->
       fprintf fmt "%a" ident id
   | App (id, tl) ->
       fprintf fmt "@[%a(%a)@]" ident id print_terms tl
 
-and print_terms fmt tl = 
+and print_terms fmt tl =
   print_list comma print_term fmt tl
 
-let rec print_predicate fmt p = 
-  let pp = print_predicate in 
+let rec print_predicate fmt p =
+  let pp = print_predicate in
   match p with
   | True ->
       fprintf fmt "true"
@@ -90,9 +90,9 @@ let rec print_predicate fmt p =
       fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b
   | Fatom (Gt (a, b)) ->
       fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b
-  | Fatom (Pred (id, [])) -> 
+  | Fatom (Pred (id, [])) ->
       fprintf fmt "%a" ident id
-  | Fatom (Pred (id, tl)) -> 
+  | Fatom (Pred (id, tl)) ->
       fprintf fmt "@[%a(%a)@]" ident id print_terms tl
   | Imp (a, b) ->
       fprintf fmt "@[(%a ->@ %a)@]" pp a pp b
@@ -104,9 +104,9 @@ let rec print_predicate fmt p =
       fprintf fmt "@[(%a or@ %a)@]" pp a pp b
   | Not a ->
       fprintf fmt "@[(not@ %a)@]" pp a
-  | Forall (id, t, p) -> 
+  | Forall (id, t, p) ->
       fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p
-  | Exists (id, t, p) -> 
+  | Exists (id, t, p) ->
       fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p
 
 let print_query fmt (decls,concl) =
@@ -117,7 +117,7 @@ let print_query fmt (decls,concl) =
 	fprintf fmt "@[type 'a %a@]@\n@\n" ident id
     | DeclType (id, n) ->
 	fprintf fmt "@[type (";
-	for i = 1 to n do 
+	for i = 1 to n do
 	  fprintf fmt "'a%d" i; if i < n then fprintf fmt ", "
 	done;
 	fprintf fmt ") %a@]@\n@\n" ident id
@@ -128,18 +128,18 @@ let print_query fmt (decls,concl) =
     | DeclFun (id, _, [], t) ->
 	fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t
     | DeclFun (id, _, l, t) ->
-	fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" 
+	fprintf fmt "@[logic %a : %a -> %a@]@\n@\n"
 	  ident id (print_list comma print_typ) l print_typ t
     | DeclPred (id, _, []) ->
 	fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id
-    | DeclPred (id, _, l) -> 
-	fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" 
+    | DeclPred (id, _, l) ->
+	fprintf fmt "@[logic %a : %a -> prop@]@\n@\n"
 	  ident id (print_list comma print_typ) l
     | DeclType _ | Axiom _ ->
 	()
   in
   let print_assert = function
-    | Axiom (id, f)  -> 
+    | Axiom (id, f)  ->
 	fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f
     | DeclType _ | DeclFun _ | DeclPred _ ->
 	()
diff --git a/plugins/dp/dp_why.mli b/plugins/dp/dp_why.mli
index b38a3d376..0efa24a23 100644
--- a/plugins/dp/dp_why.mli
+++ b/plugins/dp/dp_why.mli
@@ -7,7 +7,7 @@ val output_file : string -> query -> unit
 
 (* table to translate the proofs back to Coq (used in dp_zenon) *)
 
-type proof = 
+type proof =
   | Immediate of Term.constr
   | Fun_def of string * (string * typ) list * typ * term
 
diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
index 658534151..949e91e34 100644
--- a/plugins/dp/dp_zenon.mll
+++ b/plugins/dp/dp_zenon.mll
@@ -1,7 +1,7 @@
 
 {
 
-  open Lexing 
+  open Lexing
   open Pp
   open Util
   open Names
@@ -12,9 +12,9 @@
 
   let debug = ref false
   let set_debug b = debug := b
-  
+
   let buf = Buffer.create 1024
-    
+
   let string_of_global env ref =
     Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
 
@@ -50,15 +50,15 @@ and scan = parse
   { anomaly "malformed Zenon proof term" }
 
 and read_coq_term = parse
-| "." "\n" 
+| "." "\n"
   { let s = Buffer.contents buf in Buffer.clear buf; s }
 | "coq__" (ident as id) (* a Why keyword renamed *)
   { Buffer.add_string buf id; read_coq_term lexbuf }
-| ("dp_axiom__" ['0'-'9']+) as id 
+| ("dp_axiom__" ['0'-'9']+) as id
   { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
-| _ as c 
+| _ as c
   { Buffer.add_char buf c; read_coq_term lexbuf }
-| eof 
+| eof
   { anomaly "malformed Zenon proof term" }
 
 and read_lemma_proof = parse
@@ -71,7 +71,7 @@ and read_lemma_proof = parse
 and read_main_proof = parse
 | ":=" "\n"
   { read_coq_term lexbuf }
-| _ 
+| _
   { read_main_proof lexbuf }
 | eof
   { anomaly "malformed Zenon proof term" }
@@ -88,7 +88,7 @@ and read_main_proof = parse
     if not !debug then begin try Sys.remove f with _ -> () end;
     p
 
-  let constr_of_string gl s = 
+  let constr_of_string gl s =
     let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
     Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
 
@@ -102,7 +102,7 @@ and read_main_proof = parse
       | [] -> ()
       | [x] -> print fmt x
       | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-	  
+
     let space fmt () = fprintf fmt "@ "
     let comma fmt () = fprintf fmt ",@ "
 
@@ -110,14 +110,14 @@ and read_main_proof = parse
       | Tvar x -> fprintf fmt "%s" x
       | Tid ("int", []) -> fprintf fmt "Z"
       | Tid (x, []) -> fprintf fmt "%s" x
-      | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t 
-      | Tid (x,tl) -> 
-	  fprintf fmt "(%s %a)" x (print_list comma print_typ) tl 
-	  
+      | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t
+      | Tid (x,tl) ->
+	  fprintf fmt "(%s %a)" x (print_list comma print_typ) tl
+
     let rec print_term fmt = function
-      | Cst n -> 
+      | Cst n ->
 	  fprintf fmt "%s" (Big_int.string_of_big_int n)
-      | RCst s -> 
+      | RCst s ->
           fprintf fmt "%s" (Big_int.string_of_big_int s)
       | Power2 n ->
           fprintf fmt "@[(powerRZ 2 %s)@]" (Big_int.string_of_big_int n)
@@ -132,13 +132,13 @@ and read_main_proof = parse
       | Div (a, b) ->
 	  fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
       | Opp (a) ->
-	  fprintf fmt "@[(Zopp %a)@]" print_term a 
+	  fprintf fmt "@[(Zopp %a)@]" print_term a
       | App (id, []) ->
 	  fprintf fmt "%s" id
       | App (id, tl) ->
 	  fprintf fmt "@[(%s %a)@]" id print_terms tl
 
-    and print_terms fmt tl = 
+    and print_terms fmt tl =
       print_list space print_term fmt tl
 
     (* builds the text for "forall vars, f vars = t" *)
@@ -146,17 +146,17 @@ and read_main_proof = parse
       let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
       fprintf str_formatter
 	"@[(forall %a, %s %a = %a)@]@."
-	(print_list space binder) vars f 
+	(print_list space binder) vars f
 	(print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
 	print_term t;
       flush_str_formatter ()
-			   
+
   end
 
   let prove_axiom id = match Dp_why.find_proof id with
-    | Immediate t -> 
+    | Immediate t ->
 	exact_check t
-    | Fun_def (f, vars, ty, t) -> 
+    | Fun_def (f, vars, ty, t) ->
 	tclTHENS
 	  (fun gl ->
 	     let s = Coq.fun_def_axiom f vars t in
diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli
index 32637bb74..4fb763a6d 100644
--- a/plugins/dp/fol.mli
+++ b/plugins/dp/fol.mli
@@ -1,11 +1,11 @@
 
 (* Polymorphic First-Order Logic (that is Why's input logic) *)
 
-type typ = 
+type typ =
   | Tvar of string
   | Tid of string * typ list
 
-type term =   
+type term =
   | Cst of Big_int.big_int
   | RCst of Big_int.big_int
   | Power2 of Big_int.big_int
@@ -16,7 +16,7 @@ type term =
   | Opp of term
   | App of string * term list
 
-and atom =   
+and atom =
   | Eq of term * term
   | Le of term * term
   | Lt of term * term
@@ -24,7 +24,7 @@ and atom =
   | Gt of term * term
   | Pred of string * term list
 
-and form = 
+and form =
   | Fatom of atom
   | Imp of form * form
   | Iff of form * form
@@ -48,8 +48,8 @@ type query = decl list * form
 
 (* prover result *)
 
-type prover_answer = 
-  | Valid of string option 
+type prover_answer =
+  | Valid of string option
   | Invalid
   | DontKnow
   | Timeout
diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
index e027c882e..505b07a14 100644
--- a/plugins/dp/g_dp.ml4
+++ b/plugins/dp/g_dp.ml4
@@ -49,7 +49,7 @@ TACTIC EXTEND admit
   [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
 END
 
-VERNAC COMMAND EXTEND Dp_hint 
+VERNAC COMMAND EXTEND Dp_hint
   [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ]
 END
 
diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
index 3e4c0f6dd..0940b1352 100644
--- a/plugins/dp/test2.v
+++ b/plugins/dp/test2.v
@@ -36,7 +36,7 @@ Goal fct O = O.
  Admitted.
 
 Fixpoint even (n:nat) : Prop :=
-  match n with 
+  match n with
   O => True
   | S O => False
   | S (S p) => even p
@@ -64,9 +64,9 @@ BUG avec head prédéfini : manque eta-expansion sur A:Set
 
 Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
 
-Print value. 
+Print value.
 Print Some.
- 
+
 zenon.
 *)
 
diff --git a/plugins/dp/tests.v b/plugins/dp/tests.v
index 1a796094b..dc85d2ee2 100644
--- a/plugins/dp/tests.v
+++ b/plugins/dp/tests.v
@@ -50,8 +50,8 @@ Qed.
 Parameter nlist: list nat -> Prop.
 
 Lemma poly_1 : forall l,  nlist l -> True.
-intros. 
-simplify. 
+intros.
+simplify.
 Qed.
 
 (* user lists *)
@@ -66,8 +66,8 @@ match l with
 | cons a l1 => cons A a (app A l1 m)
 end.
 
-Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True. 
-intros; ergo. 
+Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True.
+intros; ergo.
 Qed.
 
 (* polymorphism *)
@@ -81,13 +81,13 @@ Parameter my_nlist: mylist nat -> Prop.
 
  Goal forall l,  my_nlist l -> True.
  intros.
- simplify. 
+ simplify.
 Qed.
 
 (* First example with the 0 and the equality translated *)
 
 Goal 0 = 0.
-simplify. 
+simplify.
 Qed.
 
 (* Examples in the Propositional Calculus
@@ -102,7 +102,7 @@ Qed.
 
 Goal A -> (A \/ C).
 
-simplify. 
+simplify.
 Qed.
 
 
@@ -145,12 +145,12 @@ induction x0; ergo.
 Qed.
 
 
-(* No decision procedure can solve this problem 
+(* No decision procedure can solve this problem
   Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
 *)
 
 
-(* Functions definitions *) 
+(* Functions definitions *)
 
 Definition fst (x y : Z) : Z := x.
 
@@ -205,7 +205,7 @@ Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2).
 Dp_hint add_0.
 Dp_hint add_S.
 
-(* Simplify can't prove this goal before the timeout 
+(* Simplify can't prove this goal before the timeout
    unlike zenon *)
 
 Goal forall n : nat, add n 0 = n.
@@ -258,7 +258,7 @@ Qed.
 
 (* sorts issues *)
 
-Parameter foo : Set.         
+Parameter foo : Set.
 Parameter ff : nat -> foo -> foo -> nat.
 Parameter g : foo -> foo.
 Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.