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

1 files changed, 236 insertions, 236 deletions

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 02bff3b15f..1c48988c77 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -47,18 +47,18 @@ let check_required_library d =
   let dir = make_dirpath (List.rev d') in
   if not (Library.library_is_loaded dir) then
     error ("Library "^(list_last d)^" has to be required first.")
-      
+
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
-  
+
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else check_required_library ["Coq";"Setoids";"Setoid"]
 
-let proper_class = 
+let proper_class =
   lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Proper"))))
 
-let proper_proxy_class = 
+let proper_proxy_class =
   lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy"))))
 
 let proper_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force proper_class).cl_projs))))
@@ -68,10 +68,10 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in
     Nametab.global_of_path sp
-      
+
 let try_find_reference dir s =
   constr_of_global (try_find_global_reference dir s)
-    
+
 let gen_constant dir s = Coqlib.gen_constant "rewrite" dir s
 let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
 let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
@@ -131,16 +131,16 @@ let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalenc
 
 let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation")
 let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrite_relation")
-  
-let arrow_morphism a b = 
+
+let arrow_morphism a b =
   if isprop a && isprop b then
     Lazy.force impl
   else
     mkApp(Lazy.force arrow, [|a;b|])
 
-let setoid_refl pars x = 
+let setoid_refl pars x =
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
-      
+
 let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl)
 
 let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl)
@@ -148,9 +148,9 @@ let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).c
 let is_applied_rewrite_relation env sigma rels t =
   match kind_of_term t with
   | App (c, args) when Array.length args >= 2 ->
-      let head = if isApp c then fst (destApp c) else c in 
+      let head = if isApp c then fst (destApp c) else c in
 	if eq_constr (Lazy.force coq_eq) head then None
-	else 
+	else
 	  (try
 	      let params, args = array_chop (Array.length args - 2) args in
 	      let env' = Environ.push_rel_context rels env in
@@ -160,19 +160,19 @@ let is_applied_rewrite_relation env sigma rels t =
 		Some (sigma, it_mkProd_or_LetIn t rels)
 	  with _ -> None)
   | _ -> None
-      
-let _ = 
+
+let _ =
   Equality.register_is_applied_rewrite_relation is_applied_rewrite_relation
 
 let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-let new_goal_evar (goal,cstr) env t = 
+let new_goal_evar (goal,cstr) env t =
   let goal', t = Evarutil.new_evar goal env t in
     (goal', cstr), t
 
-let new_cstr_evar (goal,cstr) env t = 
+let new_cstr_evar (goal,cstr) env t =
   let cstr', t = Evarutil.new_evar cstr env t in
     (goal, cstr'), t
 
@@ -183,7 +183,7 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
   in
   let mk_relty evars env ty obj =
     match obj with
-      | None -> 
+      | None ->
 	  let relty = mk_relation ty in
 	    new_evar evars env relty
       | Some x -> evars, f x
@@ -191,7 +191,7 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
   let rec aux env evars ty l =
     let t = Reductionops.whd_betadeltaiota env (fst evars) ty in
       match kind_of_term t, l with
-      | Prod (na, ty, b), obj :: cstrs -> 
+      | Prod (na, ty, b), obj :: cstrs ->
 	  if dependent (mkRel 1) b then
 	    let (evars, b, arg, cstrs) = aux (Environ.push_rel (na, None, ty) env) evars b cstrs in
 	    let ty = Reductionops.nf_betaiota (fst evars) ty in
@@ -207,22 +207,22 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
       | _, obj :: _ -> anomaly "build_signature: not enough products"
-      | _, [] -> 
+      | _, [] ->
 	  (match finalcstr with
-	  | None -> 
+	  | None ->
 	      let t = Reductionops.nf_betaiota (fst evars) ty in
-	      let evars, rel = mk_relty evars env t None in 
+	      let evars, rel = mk_relty evars env t None in
 		evars, t, rel, [t, Some rel]
 	  | Some codom -> let (t, rel) = codom in
 			    evars, t, rel, [t, Some rel])
   in aux env evars m cstrs
-    
+
 let proper_proof env evars carrier relation x =
   let goal = mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |])
   in new_cstr_evar evars env goal
 
 let find_class_proof proof_type proof_method env evars carrier relation =
-  try 
+  try
     let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in
     let evars, c = Typeclasses.resolve_one_typeclass env evars goal in
       mkApp (Lazy.force proof_method, [| carrier; relation; c |])
@@ -234,7 +234,7 @@ let get_transitive_proof env = find_class_proof transitive_type transitive_proof
 
 exception FoundInt of int
 
-let array_find (arr: 'a array) (pred: int -> 'a -> bool): int = 
+let array_find (arr: 'a array) (pred: int -> 'a -> bool): int =
   try
     for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done;
     raise Not_found
@@ -253,12 +253,12 @@ type hypinfo = {
 }
 
 let evd_convertible env evd x y =
-  try ignore(Evarconv.the_conv_x env x y evd); true 
+  try ignore(Evarconv.the_conv_x env x y evd); true
   with _ -> false
-  
+
 let decompose_applied_relation env sigma c left2right =
   let ctype = Typing.type_of env sigma c in
-  let find_rel ty = 
+  let find_rel ty =
     let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
     let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
     let rec split_last_two = function
@@ -267,7 +267,7 @@ let decompose_applied_relation env sigma c left2right =
 	  let l,res = split_last_two (y::z) in x::l, res
       | _ -> error "The term provided is not an applied relation." in
     let others,(c1,c2) = split_last_two args in
-    let ty1, ty2 = 
+    let ty1, ty2 =
       Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
     in
       if not (evd_convertible env eqclause.evd ty1 ty2) then None
@@ -278,12 +278,12 @@ let decompose_applied_relation env sigma c left2right =
   in
     match find_rel ctype with
     | Some c -> c
-    | None -> 
+    | None ->
 	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
 	match find_rel (it_mkProd_or_LetIn t' ctx) with
 	| Some c -> c
 	| None -> error "The term does not end with an applied homogeneous relation."
-	    
+
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
@@ -312,27 +312,27 @@ let setoid_rewrite_unif_flags = {
 
 let convertible env evd x y =
   Reductionops.is_conv env evd x y
-  
+
 let allowK = true
 
-let refresh_hypinfo env sigma hypinfo = 
+let refresh_hypinfo env sigma hypinfo =
   if hypinfo.abs = None then
     let {l2r=l2r; c=c;cl=cl} = hypinfo in
-      match c with 
+      match c with
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
 	    decompose_applied_relation env cl.evd c l2r;
 	| _ -> hypinfo
   else hypinfo
 
-let unify_eqn env sigma hypinfo t = 
+let unify_eqn env sigma hypinfo t =
   if isEvar t then None
-  else try 
+  else try
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
     let left = if l2r then c1 else c2 in
     let env', prf, c1, c2, car, rel =
       match abs with
-      | Some (absprf, absprfty) -> 
+      | Some (absprf, absprfty) ->
 	  let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
 	    env', prf, c1, c2, car, rel
       | None ->
@@ -342,7 +342,7 @@ let unify_eqn env sigma hypinfo t =
 	      (* For Ring essentially, only when doing setoid_rewrite *)
 	      clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl
 	  in
-	  let env' = 
+	  let env' =
 	    let mvs = clenv_dependent false env' in
 	      clenv_pose_metas_as_evars env' mvs
 	  in
@@ -350,13 +350,13 @@ let unify_eqn env sigma hypinfo t =
 	  let env' = { env' with evd = evd' } in
 	  let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
 	  let c1 = nf c1 and c2 = nf c2
-	  and car = nf car and rel = nf rel 
+	  and car = nf car and rel = nf rel
 	  and prf = nf (Clenv.clenv_value env') in
-	  let ty1 = Typing.mtype_of env'.env env'.evd c1 
+	  let ty1 = Typing.mtype_of env'.env env'.evd c1
 	  and ty2 = Typing.mtype_of env'.env env'.evd c2
 	  in
 	    if convertible env env'.evd ty1 ty2 then (
-	      if occur_meta prf then 
+	      if occur_meta prf then
 		hypinfo := refresh_hypinfo env sigma !hypinfo;
 	      env', prf, c1, c2, car, rel)
 	    else raise Reduction.NotConvertible
@@ -364,7 +364,7 @@ let unify_eqn env sigma hypinfo t =
     let res =
       if l2r then (prf, (car, rel, c1, c2))
       else
-	try (mkApp (get_symmetric_proof env Evd.empty car rel, 
+	try (mkApp (get_symmetric_proof env Evd.empty car rel,
 		   [| c1 ; c2 ; prf |]),
 	    (car, rel, c2, c1))
 	with Not_found ->
@@ -374,16 +374,16 @@ let unify_eqn env sigma hypinfo t =
 
 let unfold_impl t =
   match kind_of_term t with
-    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) -> 
+    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
 	mkProd (Anonymous, a, lift 1 b)
     | _ -> assert false
 
-let unfold_id t = 
+let unfold_id t =
   match kind_of_term t with
     | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_id) *) -> b
     | _ -> assert false
 
-let unfold_all t = 
+let unfold_all t =
   match kind_of_term t with
     | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
 	(match kind_of_term b with
@@ -391,7 +391,7 @@ let unfold_all t =
 	  | _ -> assert false)
     | _ -> assert false
 
-let decomp_prod env evm n c = 
+let decomp_prod env evm n c =
   snd (Reductionops.splay_prod_n env evm n c)
 
 let rec decomp_pointwise n c =
@@ -400,19 +400,19 @@ let rec decomp_pointwise n c =
     match kind_of_term c with
       | App (pointwise, [| a; b; relb |]) -> decomp_pointwise (pred n) relb
       | _ -> raise Not_found
-	  
+
 let lift_cstr env sigma evars args cstr =
   let cstr =
-    let start = 
+    let start =
       match cstr with
       | Some codom -> codom
-      | None -> 
+      | None ->
 	  let car = Evarutil.e_new_evar evars env (new_Type ()) in
 	  let rel = Evarutil.e_new_evar evars env (mk_relation car) in
 	    (car, rel)
     in
       Array.fold_right
-	(fun arg (car, rel) -> 
+	(fun arg (car, rel) ->
 	  let ty = Typing.type_of env sigma arg in
 	  let car' = mkProd (Anonymous, ty, car) in
 	  let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in
@@ -440,10 +440,10 @@ type rewrite_result_info = {
 }
 
 type rewrite_result = rewrite_result_info option
-  
+
 type strategy = Environ.env -> evar_defs -> constr -> types ->
   constr option -> evars -> rewrite_result option
-  
+
 let resolve_subrelation env sigma car rel rel' res =
   if eq_constr rel rel' then res
   else
@@ -452,14 +452,14 @@ let resolve_subrelation env sigma car rel rel' res =
 (*   with NotConvertible -> *)
     let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
     let evars, subrel = new_cstr_evar res.rew_evars env app in
-      { res with 
+      { res with
 	rew_prf = mkApp (subrel, [| res.rew_from ; res.rew_to ; res.rew_prf |]);
 	rew_rel = rel';
 	rew_evars = evars }
 
 
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
-  let evars, morph_instance, proj, sigargs, m', args, args' = 
+  let evars, morph_instance, proj, sigargs, m', args, args' =
     let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
     let morphargs, morphobjs = array_chop first args in
     let morphargs', morphobjs' = array_chop first args' in
@@ -477,22 +477,22 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
     in
     let evars, morph = new_cstr_evar evars env' app in
       evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
-  in 
-  let projargs, subst, evars, respars, typeargs = 
-    array_fold_left2 
-      (fun (acc, subst, evars, sigargs, typeargs') x y -> 
+  in
+  let projargs, subst, evars, respars, typeargs =
+    array_fold_left2
+      (fun (acc, subst, evars, sigargs, typeargs') x y ->
 	let (carrier, relation), sigargs = split_head sigargs in
 	  match relation with
 	  | Some relation ->
-	      let carrier = substl subst carrier 
+	      let carrier = substl subst carrier
 	      and relation = substl subst relation in
 	      (match y with
 	      | None ->
 		  let evars, proof = proper_proof env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
-	      | Some r -> 
+	      | Some r ->
 		  [ r.rew_prf; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs')
-	  | None -> 
+	  | None ->
 	      if y <> None then error "Cannot rewrite the argument of a dependent function";
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
@@ -502,7 +502,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
     match respars with
 	[ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt
       | _ -> assert(false)
-	
+
 let apply_constraint env sigma car rel cstr res =
   match cstr with
   | None -> res
@@ -512,7 +512,7 @@ let eq_env x y = x == y
 
 let apply_rule hypinfo loccs : strategy =
   let (nowhere_except_in,occs) = loccs in
-  let is_occ occ = 
+  let is_occ occ =
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
   let occ = ref 0 in
     fun env sigma t ty cstr evars ->
@@ -520,13 +520,13 @@ let apply_rule hypinfo loccs : strategy =
       let unif = unify_eqn env sigma hypinfo t in
 	if unif <> None then incr occ;
 	match unif with
-	| Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ -> 
+	| Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ ->
 	    begin
 	      let goalevars = Evd.evar_merge (fst evars)
 		(Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd))
 	      in
-	      let res = { rew_car = ty; rew_rel = rel; rew_from = c1; 
-			  rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars } 
+	      let res = { rew_car = ty; rew_rel = rel; rew_from = c1;
+			  rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars }
 	      in Some (Some (apply_constraint env sigma car rel cstr res))
 	    end
 	| _ -> None
@@ -538,27 +538,27 @@ let apply_lemma (evm,c) left2right loccs : strategy =
       apply_rule hypinfo loccs env sigma
 
 let make_leibniz_proof c ty r =
-  let prf = mkApp (Lazy.force coq_f_equal, 
+  let prf = mkApp (Lazy.force coq_f_equal,
 		  [| r.rew_car; ty;
 		     mkLambda (Anonymous, r.rew_car, c (mkRel 1));
 		     r.rew_from; r.rew_to; r.rew_prf |])
   in
-    { r with rew_car = ty; rew_rel = mkApp (Lazy.force coq_eq, [| ty |]); 
+    { r with rew_car = ty; rew_rel = mkApp (Lazy.force coq_eq, [| ty |]);
       rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf }
-      
+
 let subterm all flags (s : strategy) : strategy =
   let rec aux env sigma t ty cstr evars =
     let cstr' = Option.map (fun c -> (ty, c)) cstr in
       match kind_of_term t with
       | App (m, args) ->
-	  let rewrite_args success = 
+	  let rewrite_args success =
 	    let args', evars', progress =
-	      Array.fold_left 
-		(fun (acc, evars, progress) arg -> 
+	      Array.fold_left
+		(fun (acc, evars, progress) arg ->
 		  if progress <> None && not all then (None :: acc, evars, progress)
-		  else 
+		  else
 		    let res = s env sigma arg (Typing.type_of env sigma arg) None evars in
-		      match res with 
+		      match res with
 		      | Some None -> (None :: acc, evars, if progress = None then Some false else progress)
 		      | Some (Some r) -> (Some r :: acc, r.rew_evars, Some true)
 		      | None -> (None :: acc, evars, progress))
@@ -573,11 +573,11 @@ let subterm all flags (s : strategy) : strategy =
 		  let res = { rew_car = ty; rew_rel = rel; rew_from = c1;
 			      rew_to = c2; rew_prf = prf; rew_evars = evars' } in
 		    Some (Some res)
-	  in 
+	  in
 	    if flags.on_morphisms then
 	      let evarsref = ref (snd evars) in
 	      let cstr' = lift_cstr env sigma evarsref args cstr' in
-	      let m' = s env sigma m (Typing.type_of env sigma m) 
+	      let m' = s env sigma m (Typing.type_of env sigma m)
 		(Option.map snd cstr') (fst evars, !evarsref)
 	      in
 		match m' with
@@ -587,14 +587,14 @@ let subterm all flags (s : strategy) : strategy =
 		    (* We rewrote the function and get a proof of pointwise rel for the arguments.
 		       We just apply it. *)
 		    let nargs = Array.length args in
-		    let res = 
+		    let res =
 		      { rew_car = decomp_prod env (fst r.rew_evars) nargs r.rew_car;
-			rew_rel = decomp_pointwise nargs r.rew_rel; 
+			rew_rel = decomp_pointwise nargs r.rew_rel;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
 			rew_prf = mkApp (r.rew_prf, args); rew_evars = r.rew_evars }
 		    in Some (Some res)
 	    else rewrite_args None
-	      
+
       | Prod (n, x, b) when not (dependent (mkRel 1) b) ->
 	  let b = subst1 mkProp b in
 	  let tx = Typing.type_of env sigma x and tb = Typing.type_of env sigma b in
@@ -602,7 +602,7 @@ let subterm all flags (s : strategy) : strategy =
 	    (match res with
 	    | Some (Some r) -> Some (Some { r with rew_to = unfold_impl r.rew_to })
 	    | _ -> res)
-	      
+
       (* 		if x' = None && flags.under_lambdas then *)
       (* 		  let lam = mkLambda (n, x, b) in *)
       (* 		  let lam', occ = aux env lam occ None in *)
@@ -616,14 +616,14 @@ let subterm all flags (s : strategy) : strategy =
       (* 				 cstr evars) *)
       (* 		  in res, occ *)
       (* 		else *)
-	      
+
       | Prod (n, dom, codom) when eq_constr ty mkProp ->
 	  let lam = mkLambda (n, dom, codom) in
 	  let res = aux env sigma (mkApp (Lazy.force coq_all, [| dom; lam |])) ty cstr evars in
 	    (match res with
 	    | Some (Some r) -> Some (Some { r with rew_to = unfold_all r.rew_to })
 	    | _ -> res)
-	      
+
       | Lambda (n, t, b) when flags.under_lambdas ->
 	  let env' = Environ.push_rel (n, None, t) env in
 	  let b' = s env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
@@ -636,7 +636,7 @@ let subterm all flags (s : strategy) : strategy =
 		  rew_from = mkLambda(n, t, r.rew_from);
 		  rew_to = mkLambda (n, t, r.rew_to) })
 	    | _ -> b')
-	      
+
       | Case (ci, p, c, brs) ->
 	  let cty = Typing.type_of env sigma c in
 	  let cstr = Some (mkApp (Lazy.force coq_eq, [| cty |])) in
@@ -644,16 +644,16 @@ let subterm all flags (s : strategy) : strategy =
 	    (match c' with
 	    | Some (Some r) ->
 		Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
-	    | x -> 
+	    | x ->
 		if array_for_all ((=) 0) ci.ci_cstr_nargs then
 		  let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
-		  let found, brs' = Array.fold_left (fun (found, acc) br -> 
-		    if found <> None then (found, fun x -> br :: acc x) 
+		  let found, brs' = Array.fold_left (fun (found, acc) br ->
+		    if found <> None then (found, fun x -> br :: acc x)
 		    else
 		      match s env sigma br ty cstr evars with
 		      | Some (Some r) -> (Some r, fun x -> x :: acc x)
-		      | _ -> (None, fun x -> br :: acc x)) 
-		    (None, fun x -> []) brs 
+		      | _ -> (None, fun x -> br :: acc x))
+		    (None, fun x -> []) brs
 		  in
 		    match found with
 		    | Some r ->
@@ -674,7 +674,7 @@ let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewri
   match next env sigma res.rew_to res.rew_car (Some res.rew_rel) res.rew_evars with
   | None -> None
   | Some None -> Some (Some res)
-  | Some (Some res') -> 
+  | Some (Some res') ->
       let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car ; res.rew_rel |]) in
       let evars, prf = new_cstr_evar res'.rew_evars env prfty in
       let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
@@ -682,22 +682,22 @@ let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewri
       in Some (Some { res' with rew_from = res.rew_from; rew_evars = evars; rew_prf = prf })
 
 (** Rewriting strategies.
-    
+
     Inspired by ELAN's rewriting strategies:
     http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.4049
 *)
 
-module Strategies = 
+module Strategies =
   struct
 
-    let fail : strategy = 
+    let fail : strategy =
       fun env sigma t ty cstr evars -> None
 
-    let id : strategy = 
+    let id : strategy =
       fun env sigma t ty cstr evars -> Some None
 
     let refl : strategy =
-      fun env sigma t ty cstr evars -> 
+      fun env sigma t ty cstr evars ->
 	let evars, rel = match cstr with
 	  | None -> new_cstr_evar evars env (mk_relation ty)
 	  | Some r -> evars, r
@@ -706,11 +706,11 @@ module Strategies =
 	  let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in
 	    new_cstr_evar evars env mty
 	in
-	  Some (Some { rew_car = ty; rew_rel = rel; rew_from = t; rew_to = t; 
+	  Some (Some { rew_car = ty; rew_rel = rel; rew_from = t; rew_to = t;
 		       rew_prf = proof; rew_evars = evars })
-	    
+
     let progress (s : strategy) : strategy =
-      fun env sigma t ty cstr evars -> 
+      fun env sigma t ty cstr evars ->
 	match s env sigma t ty cstr evars with
 	| None -> None
 	| Some None -> None
@@ -722,7 +722,7 @@ module Strategies =
 	| None -> None
 	| Some None -> snd env sigma t ty cstr evars
 	| Some (Some res) -> transitivity env sigma res snd
-	    
+
     let choice fst snd : strategy =
       fun env sigma t ty cstr evars ->
 	match fst env sigma t ty cstr evars with
@@ -731,7 +731,7 @@ module Strategies =
 
     let try_ str : strategy = choice str id
 
-    let fix (f : strategy -> strategy) : strategy = 
+    let fix (f : strategy -> strategy) : strategy =
       let rec aux env = f (fun env -> aux env) env in aux
 
     let any (s : strategy) : strategy =
@@ -740,10 +740,10 @@ module Strategies =
     let repeat (s : strategy) : strategy =
       seq s (any s)
 
-    let bu (s : strategy) : strategy = 
+    let bu (s : strategy) : strategy =
       fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
 
-    let td (s : strategy) : strategy = 
+    let td (s : strategy) : strategy =
       fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
 
     let innermost (s : strategy) : strategy =
@@ -756,7 +756,7 @@ module Strategies =
       List.fold_left (fun tac (l,l2r) ->
 	choice tac (apply_lemma l l2r (false,[])))
 	fail cs
-	
+
     let old_hints (db : string) : strategy =
       let rules = Autorewrite.find_rewrites db in
 	lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
@@ -771,9 +771,9 @@ end
 
 (** The strategy for a single rewrite, dealing with occurences. *)
 
-let rewrite_strat flags occs hyp = 
+let rewrite_strat flags occs hyp =
   let app = apply_rule hyp occs in
-  let rec aux () = 
+  let rec aux () =
     Strategies.choice app (subterm true flags (fun env -> aux () env))
   in aux ()
 
@@ -791,26 +791,26 @@ let apply_strategy (s : strategy) env sigma concl cstr evars =
     match res with
     | None -> None
     | Some None -> Some None
-    | Some (Some res) -> 
+    | Some (Some res) ->
 	evars := res.rew_evars;
 	Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to)))
 
-let split_evars_once sigma evd = 
+let split_evars_once sigma evd =
   Evd.fold (fun ev evi deps ->
-    if Intset.mem ev deps then 
+    if Intset.mem ev deps then
       Intset.union (Class_tactics.evars_of_evi evi) deps
     else deps) evd sigma
-    
+
 let existentials_of_evd evd =
-  Evd.fold (fun ev evi acc -> Intset.add ev acc) evd Intset.empty 
+  Evd.fold (fun ev evi acc -> Intset.add ev acc) evd Intset.empty
 
 let evd_of_existentials evd exs =
-  Intset.fold (fun i acc -> 
+  Intset.fold (fun i acc ->
     let evi = Evd.find evd i in
       Evd.add acc i evi) exs Evd.empty
 
-let split_evars sigma evd = 
-  let rec aux deps = 
+let split_evars sigma evd =
+  let rec aux deps =
     let deps' = split_evars_once deps evd in
       if Intset.equal deps' deps then
 	evd_of_existentials evd deps
@@ -822,12 +822,12 @@ let solve_constraints env evars =
   Typeclasses.resolve_typeclasses env ~split:false ~fail:true (merge_evars evars)
 
 let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
-  let concl, is_hyp = 
+  let concl, is_hyp =
     match clause with
 	Some id -> pf_get_hyp_typ gl id, Some id
       | None -> pf_concl gl, None
   in
-  let cstr = 
+  let cstr =
     let sort = mkProp in
     let impl = Lazy.force impl in
       match is_hyp with
@@ -839,34 +839,34 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
   let env = pf_env gl in
   let eq = apply_strategy strat env sigma concl (Some cstr) evars in
     match eq with
-    | Some (Some (p, (_, _, oldt, newt))) -> 
+    | Some (Some (p, (_, _, oldt, newt))) ->
 	(try
 	    let cstrevars = !evars in
 	    let evars = solve_constraints env cstrevars in
 	    let p = Evarutil.nf_isevar evars p in
 	    let newt = Evarutil.nf_isevar evars newt in
-	    let abs = Option.map (fun (x, y) -> 
+	    let abs = Option.map (fun (x, y) ->
 	      Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in
 	    let undef = split_evars (fst cstrevars) evars in
-	    let rewtac = 
+	    let rewtac =
 	      match is_hyp with
-	      | Some id -> 
-		  let term = 
+	      | Some id ->
+		  let term =
 		    match abs with
 		    | None -> p
-		    | Some (t, ty) -> 
+		    | Some (t, ty) ->
 			mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
 		  in
-		    cut_replacing id newt 
+		    cut_replacing id newt
 		      (fun x -> Tacmach.refine_no_check (mkApp (term, [| mkVar id |])))
-	      | None -> 
+	      | None ->
 		  (match abs with
-		  | None -> 
+		  | None ->
 		      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
 			tclTHENLAST
 			  (Tacmach.internal_cut_no_check false name newt)
 			  (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p))
-		  | Some (t, ty) -> 
+		  | Some (t, ty) ->
 		      Tacmach.refine_no_check
 			(mkApp (mkLambda (Name (id_of_string "newt"), newt,
 					 mkLambda (Name (id_of_string "lemma"), ty,
@@ -874,20 +874,20 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 			       [| mkMeta goal_meta; t |])))
 	    in
 	    let evartac =
-	      if not (undef = Evd.empty) then 
+	      if not (undef = Evd.empty) then
 		Refiner.tclEVARS undef
 	      else tclIDTAC
 	    in tclTHENLIST [evartac; rewtac] gl
-	  with 
+	  with
 	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
 	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	      Refiner.tclFAIL_lazy 0 
-		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." 
+	      Refiner.tclFAIL_lazy 0
+		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
 			++ fnl () ++ Himsg.explain_typeclass_error env e)) gl)
-    | Some None -> 
+    | Some None ->
 	tclFAIL 0 (str"setoid rewrite failed: no progress made") gl
     | None -> raise Not_found
-	
+
 let cl_rewrite_clause_strat strat clause gl =
   init_setoid ();
   let meta = Evarutil.new_meta() in
@@ -910,7 +910,7 @@ open Extraargs
 
 let occurrences_of = function
   | n::_ as nl when n < 0 -> (false,List.map abs nl)
-  | nl -> 
+  | nl ->
       if List.exists (fun n -> n < 0) nl then
 	error "Illegal negative occurrence number.";
       (true,nl)
@@ -924,7 +924,7 @@ let interp_strategy ist gl c = c
 let glob_strategy ist l = l
 let subst_strategy evm l = l
 
-let apply_constr_expr c l2r occs = fun env sigma -> 
+let apply_constr_expr c l2r occs = fun env sigma ->
   let c = Constrintern.interp_open_constr sigma env c in
     apply_lemma c l2r occs env sigma
 
@@ -985,8 +985,8 @@ END
 
 let clsubstitute o c =
   let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl 
-      (fun cl -> 
+    Tacticals.onAllHypsAndConcl
+      (fun cl ->
 	match cl with
 	  | Some id when is_tac id -> tclIDTAC
 	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
@@ -997,7 +997,7 @@ END
 
 
 (* Compatibility with old Setoids *)
-  
+
 TACTIC EXTEND setoid_rewrite
    [ "setoid_rewrite" orient(o) open_constr(c) ]
    -> [ cl_rewrite_clause c o all_occurrences None ]
@@ -1019,73 +1019,73 @@ let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_stri
 
 let declare_an_instance n s args =
   ((dummy_loc,Name n), Explicit,
-  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
+  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance binders instance fields = 
+let anew_instance binders instance fields =
   new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
     Library.require_library [qualid] (Some false)
 
-let declare_instance_refl binders a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" 
-  in anew_instance binders instance 
+let declare_instance_refl binders a aeq n lemma =
+  let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
+  in anew_instance binders instance
        [((dummy_loc,id_of_string "reflexivity"),lemma)]
 
-let declare_instance_sym binders a aeq n lemma = 
+let declare_instance_sym binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
-  in anew_instance binders instance 
+  in anew_instance binders instance
        [((dummy_loc,id_of_string "symmetry"),lemma)]
 
-let declare_instance_trans binders a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" 
-  in anew_instance binders instance 
+let declare_instance_trans binders a aeq n lemma =
+  let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
+  in anew_instance binders instance
        [((dummy_loc,id_of_string "transitivity"),lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
-let declare_relation ?(binders=[]) a aeq n refl symm trans = 
+let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
   in ignore(anew_instance binders instance []);
-  match (refl,symm,trans) with 
+  match (refl,symm,trans) with
       (None, None, None) -> ()
-    | (Some lemma1, None, None) -> 
+    | (Some lemma1, None, None) ->
 	ignore (declare_instance_refl binders a aeq n lemma1)
-    | (None, Some lemma2, None) -> 
+    | (None, Some lemma2, None) ->
 	ignore (declare_instance_sym binders a aeq n lemma2)
-    | (None, None, Some lemma3) -> 
+    | (None, None, Some lemma3) ->
 	ignore (declare_instance_trans binders a aeq n lemma3)
-    | (Some lemma1, Some lemma2, None) -> 
-	ignore (declare_instance_refl binders a aeq n lemma1); 
+    | (Some lemma1, Some lemma2, None) ->
+	ignore (declare_instance_refl binders a aeq n lemma1);
 	ignore (declare_instance_sym binders a aeq n lemma2)
-    | (Some lemma1, None, Some lemma3) -> 
+    | (Some lemma1, None, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in
 	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
-	    anew_instance binders instance 
+	    anew_instance binders instance
 	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
 	       ((dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)])
-    | (None, Some lemma2, Some lemma3) -> 
+    | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
-	    anew_instance binders instance 
+	    anew_instance binders instance
 	      [((dummy_loc,id_of_string "PER_Symmetric"), lemma2);
 	       ((dummy_loc,id_of_string "PER_Transitive"),lemma3)])
-     | (Some lemma1, Some lemma2, Some lemma3) -> 
-	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
+     | (Some lemma1, Some lemma2, Some lemma3) ->
+	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
-	  anew_instance binders instance 
+	  anew_instance binders instance
 	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
 	     ((dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
 	     ((dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
@@ -1100,19 +1100,19 @@ let (wit_binders_let : Genarg.tlevel binders_let_argtype),
 open Pcoq.Constr
 
 VERNAC COMMAND EXTEND AddRelation
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
 
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)  
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
 	"as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) None None ]
-  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] -> 
+  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
       [ declare_relation a aeq n None None None ]
 END
 
 VERNAC COMMAND EXTEND AddRelation2
-    [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) 
+    [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       [ declare_relation a aeq n None (Some lemma2) None ]
   | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
@@ -1120,33 +1120,33 @@ VERNAC COMMAND EXTEND AddRelation2
 END
 
 VERNAC COMMAND EXTEND AddRelation3
-    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ]
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
-      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) 
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] 
+      [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
   | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
-	"as" ident(n) ] ->  
-      [ declare_relation a aeq n None None (Some lemma3) ] 
+	"as" ident(n) ] ->
+      [ declare_relation a aeq n None None (Some lemma3) ]
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation
   | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
-	"reflexivity" "proved" "by" constr(lemma1) 
+	"reflexivity" "proved" "by" constr(lemma1)
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
   | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
-	"reflexivity" "proved" "by" constr(lemma1)  
+	"reflexivity" "proved" "by" constr(lemma1)
 	"as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)  "as" ident(n) ] -> 
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None None None ]
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2
-    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) 
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
   | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
@@ -1154,16 +1154,16 @@ VERNAC COMMAND EXTEND AddParametricRelation2
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3
-    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
-      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) 
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] 
+      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
   | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
-	"as" ident(n) ] ->  
-      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] 
+	"as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
 
 let mk_qualid s =
@@ -1178,10 +1178,10 @@ let proper_projection r ty =
   let ctx, inst = decompose_prod_assum ty in
   let mor, args = destApp inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
-  let app = mkApp (Lazy.force proper_proj, 
+  let app = mkApp (Lazy.force proper_proj,
 		  Array.append args [| instarg |]) in
     it_mkLambda_or_LetIn app ctx
-      
+
 let declare_projection n instance_id r =
   let ty = Global.type_of_global r in
   let c = constr_of_global r in
@@ -1189,41 +1189,41 @@ let declare_projection n instance_id r =
   let typ = Typing.type_of (Global.env ()) Evd.empty term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
-    let n = 
-      let rec aux t = 
+    let n =
+      let rec aux t =
 	match kind_of_term t with
-	    App (f, [| a ; a' ; rel; rel' |]) when eq_constr f (Lazy.force respectful) -> 
+	    App (f, [| a ; a' ; rel; rel' |]) when eq_constr f (Lazy.force respectful) ->
 	      succ (aux rel')
 	  | _ -> 0
       in
-      let init = 
+      let init =
 	match kind_of_term typ with
-	    App (f, args) when eq_constr f (Lazy.force respectful) -> 
+	    App (f, args) when eq_constr f (Lazy.force respectful) ->
 	      mkApp (f, fst (array_chop (Array.length args - 2) args))
 	  | _ -> typ
       in aux init
     in
     let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
-    in it_mkProd_or_LetIn ccl ctx 
+    in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let cst = 
+  let cst =
     { const_entry_body = term;
       const_entry_type = Some typ;
       const_entry_opaque = false;
       const_entry_boxed = false }
   in
     ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
-          
+
 let build_morphism_signature m =
   let env = Global.env () in
   let m = Constrintern.interp_constr Evd.empty env m in
   let t = Typing.type_of env Evd.empty m in
   let isevars = ref (Evd.empty, Evd.empty) in
-  let cstrs = 
-    let rec aux t = 
+  let cstrs =
+    let rec aux t =
       match kind_of_term t with
-	| Prod (na, a, b) -> 
+	| Prod (na, a, b) ->
 	    None :: aux b
 	| _ -> []
     in aux t
@@ -1231,7 +1231,7 @@ let build_morphism_signature m =
   let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None snd in
   let _ = isevars := evars in
   let _ = List.iter
-    (fun (ty, rel) -> 
+    (fun (ty, rel) ->
       Option.iter (fun rel ->
 	let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
 	let evars,c = new_cstr_evar !isevars env default in
@@ -1239,13 +1239,13 @@ let build_morphism_signature m =
 	rel)
     cstrs
   in
-  let morph = 
+  let morph =
     mkApp (Lazy.force proper_type, [| t; sig_; m |])
   in
   let evd = solve_constraints env !isevars in
   let m = Evarutil.nf_isevar evd morph in
     Evarutil.check_evars env Evd.empty evd m; m
-	
+
 let default_morphism sign m =
   let env = Global.env () in
   let t = Typing.type_of env Evd.empty m in
@@ -1257,10 +1257,10 @@ let default_morphism sign m =
   in
   let evars, mor = resolve_one_typeclass env (merge_evars evars) morph in
     mor, proper_projection mor morph
-    	  
+
 let add_setoid binders a aeq t n =
   init_setoid ();
-  let _lemma_refl = declare_instance_refl binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
+  let _lemma_refl = declare_instance_refl binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
   let _lemma_sym = declare_instance_sym binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
   let _lemma_trans = declare_instance_trans binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
@@ -1274,7 +1274,7 @@ let add_morphism_infer glob m n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance = build_morphism_signature m in
-    if Lib.is_modtype () then 
+    if Lib.is_modtype () then
       let cst = Declare.declare_internal_constant instance_id
 				(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
@@ -1282,30 +1282,30 @@ let add_morphism_infer glob m n =
 				declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	Flags.silently 
+	Flags.silently
 	  (fun () ->
-	    Command.start_proof instance_id kind instance 
+	    Command.start_proof instance_id kind instance
 	      (fun _ -> function
-		Libnames.ConstRef cst -> 
-		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None 
+		Libnames.ConstRef cst ->
+		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
 				   glob cst);
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
-	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () 
-	  
+	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
+
 let add_morphism glob binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
-  let instance = 
+  let instance =
     ((dummy_loc,Name instance_id), Explicit,
-    CAppExpl (dummy_loc, 
-	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")), 
+    CAppExpl (dummy_loc,
+	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
 	     [cHole; s; m]))
-  in	  
+  in
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance ~global:glob binders instance (CRecord (dummy_loc,None,[]))
-	      ~generalize:false ~tac 
+	      ~generalize:false ~tac
 	      ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None)
 
 VERNAC COMMAND EXTEND AddSetoid1
@@ -1317,8 +1317,8 @@ VERNAC COMMAND EXTEND AddSetoid1
       [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
       [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
-  | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m) 
-	"with" "signature" lconstr(s) "as" ident(n) ] -> 
+  | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m)
+	"with" "signature" lconstr(s) "as" ident(n) ] ->
       [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
 END
 
@@ -1347,7 +1347,7 @@ let check_evar_map_of_evars_defs evd =
          check_freemetas_is_empty rebus2 freemetas2
    ) metas
 
-let unification_rewrite l2r c1 c2 cl car rel but gl = 
+let unification_rewrite l2r c1 c2 cl car rel but gl =
   let env = pf_env gl in
   let (evd',c') =
     try
@@ -1375,11 +1375,11 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
-let get_hyp gl evars (evm,c) clause l2r = 
+let get_hyp gl evars (evm,c) clause l2r =
   let hi = decompose_applied_relation (pf_env gl) evars c l2r in
   let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
     unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
-	
+
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
 let apply_lemma gl (evm,c) cl l2r occs =
@@ -1387,10 +1387,10 @@ let apply_lemma gl (evm,c) cl l2r occs =
   let evars = Evd.merge sigma evm in
   let hypinfo = ref (get_hyp gl evars (evm,c) cl l2r) in
   let app = apply_rule hypinfo occs in
-  let rec aux () = 
+  let rec aux () =
     Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
   in !hypinfo, aux ()
-	
+
 let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo, strat = apply_lemma gl c cl l2r occs in
@@ -1406,7 +1406,7 @@ let general_s_rewrite_clause x =
   match x with
     | None -> general_s_rewrite None
     | Some id -> general_s_rewrite (Some id)
-	
+
 let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
 
 let is_loaded d =
@@ -1421,24 +1421,24 @@ let try_loaded f gl =
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let not_declared env ty rel =
-  tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ 
+  tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++
 		str ty ++ str" relation. Maybe you need to require the Setoid library")
 
-let relation_of_constr env c = 
+let relation_of_constr env c =
   match kind_of_term c with
-    | App (f, args) when Array.length args >= 2 -> 
+    | App (f, args) when Array.length args >= 2 ->
 	let relargs, args = array_chop (Array.length args - 2) args in
 	  mkApp (f, relargs), args
-    | _ -> errorlabstrm "relation_of_constr" 
+    | _ -> errorlabstrm "relation_of_constr"
 	(str "The term " ++ Printer.pr_constr_env env c ++ str" is not an applied relation.")
-	
+
 let setoid_proof gl ty fn fallback =
   let env = pf_env gl in
-    try 
+    try
       let rel, args = relation_of_constr env (pf_concl gl) in
       let evm, car = project gl, pf_type_of gl args.(0) in
 	fn env evm car rel gl
-    with e -> 
+    with e ->
       try fallback gl
       with Hipattern.NoEquationFound ->
 	  match e with
@@ -1446,19 +1446,19 @@ let setoid_proof gl ty fn fallback =
 	      let rel, args = relation_of_constr env (pf_concl gl) in
 		not_declared env ty rel gl
 	  | _ -> raise e
-	      
+
 let setoid_reflexivity gl =
-  setoid_proof gl "reflexive" 
+  setoid_proof gl "reflexive"
     (fun env evm car rel -> apply (get_reflexive_proof env evm car rel))
     (reflexivity_red true)
-	  
+
 let setoid_symmetry gl =
-  setoid_proof gl "symmetric" 
+  setoid_proof gl "symmetric"
     (fun env evm car rel -> apply (get_symmetric_proof env evm car rel))
     (symmetry_red true)
-    
+
 let setoid_transitivity c gl =
-  setoid_proof gl "transitive" 
+  setoid_proof gl "transitive"
     (fun env evm car rel ->
       let proof = get_transitive_proof env evm car rel in
       match c with
@@ -1466,7 +1466,7 @@ let setoid_transitivity c gl =
       | Some c ->
 	  apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
     (transitivity_red true c)
-    
+
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum ctype in
@@ -1507,12 +1507,12 @@ END
 let implify id gl =
   let (_, b, ctype) = pf_get_hyp gl id in
   let binders,concl = decompose_prod_assum ctype in
-  let ctype' = 
+  let ctype' =
     match binders with
-    | (_, None, ty as hd) :: tl when not (dependent (mkRel 1) concl) -> 
+    | (_, None, ty as hd) :: tl when not (dependent (mkRel 1) concl) ->
 	let env = Environ.push_rel_context tl (pf_env gl) in
 	let sigma = project gl in
-	let tyhd = Typing.type_of env sigma ty 
+	let tyhd = Typing.type_of env sigma ty
 	and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in
 	let app = mkApp (arrow_morphism tyhd (subst1 mkProp tyconcl), [| ty; (subst1 mkProp concl) |]) in
 	  it_mkProd_or_LetIn app tl