1 files changed, 187 insertions, 187 deletions

diff --git a/AAC_coq.ml b/AAC_coq.ml
index cbe4beb..b3ee180 100644
--- a/AAC_coq.ml
+++ b/AAC_coq.ml
@@ -14,7 +14,7 @@ open Names
 open Coqlib
 
 (* The contrib name is used to locate errors when loading constrs *)
-let contrib_name = "aac_tactics" 
+let contrib_name = "aac_tactics"
 
 (* Getting constrs (primitive Coq terms) from existing Coq
    libraries. *)
@@ -25,93 +25,93 @@ let init_constant dir s = find_constant contrib_name dir s
 
 (* A clause specifying that the [let] should not try to fold anything
    in the goal *)
-let nowhere = 
-  { Tacexpr.onhyps = Some []; 
-    Tacexpr.concl_occs = Rawterm.no_occurrences_expr 
+let nowhere =
+  { Tacexpr.onhyps = Some [];
+    Tacexpr.concl_occs = Rawterm.no_occurrences_expr
   }
 
-let cps_mk_letin 
+let cps_mk_letin
     (name:string)
     (c: constr)
-    (k : constr -> Proof_type.tactic) 
+    (k : constr -> Proof_type.tactic)
 : Proof_type.tactic =
-  fun goal -> 
+  fun goal ->
     let name = (Names.id_of_string name) in
-    let name =  Tactics.fresh_id [] name goal in 
-    let letin = (Tactics.letin_tac None  (Name name) c None nowhere) in 
+    let name =  Tactics.fresh_id [] name goal in
+    let letin = (Tactics.letin_tac None  (Name name) c None nowhere) in
       Tacticals.tclTHEN letin (k (mkVar name)) goal
 
 (** {2 General functions}  *)
 
-type goal_sigma =  Proof_type.goal Tacmach.sigma 
+type goal_sigma =  Proof_type.goal Tacmach.sigma
 let goal_update (goal : goal_sigma) evar_map : goal_sigma=
-  let it = Tacmach.sig_it goal in 
-    Tacmach.re_sig it evar_map 
+  let it = Tacmach.sig_it goal in
+    Tacmach.re_sig it evar_map
 
 let fresh_evar goal ty : constr * goal_sigma =
-  let env = Tacmach.pf_env goal in 
-  let evar_map = Tacmach.project goal in 
-  let (em,x) = Evarutil.new_evar evar_map env ty in 
+  let env = Tacmach.pf_env goal in
+  let evar_map = Tacmach.project goal in
+  let (em,x) = Evarutil.new_evar evar_map env ty in
     x,( goal_update goal em)
-      
+     
 let resolve_one_typeclass goal ty : constr*goal_sigma=
-  let env = Tacmach.pf_env goal in 
-  let evar_map = Tacmach.project goal in 
-  let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in 
+  let env = Tacmach.pf_env goal in
+  let evar_map = Tacmach.project goal in
+  let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in
     c, (goal_update goal em)
 
 let general_error =
   "Cannot resolve a typeclass : please report"
 
-let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr  -> Proof_type.tactic) -> Proof_type.tactic = fun t k  goal  -> 
-  Tacmach.pf_apply 
-    (fun env em -> let em ,c =   
-		  try Typeclasses.resolve_one_typeclass env em t 
-		  with Not_found -> 
-		    begin match error with 
+let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr  -> Proof_type.tactic) -> Proof_type.tactic = fun t k  goal  ->
+  Tacmach.pf_apply
+    (fun env em -> let em ,c =  
+		  try Typeclasses.resolve_one_typeclass env em t
+		  with Not_found ->
+		    begin match error with
 		      | None -> Util.anomaly  "Cannot resolve a typeclass : please report"
 		      | Some x -> Util.error x
 		    end
-		in 
+		in
 		Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal
     )	goal
 
 
-let nf_evar goal c : Term.constr= 
-  let evar_map = Tacmach.project goal in 
+let nf_evar goal c : Term.constr=
+  let evar_map = Tacmach.project goal in
     Evarutil.nf_evar evar_map c
 
-let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma = 
-  let env = Tacmach.pf_env gl in 
-  let evar_map = Tacmach.project gl in 
-  let (em,x) = Evarutil.new_evar evar_map env x in 
+let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma =
+  let env = Tacmach.pf_env gl in
+  let evar_map = Tacmach.project gl in
+  let (em,x) = Evarutil.new_evar evar_map env x in
     x,(goal_update gl em)
-      
-let evar_binary (gl: goal_sigma) (x : constr) = 
-  let env = Tacmach.pf_env gl in 
-  let evar_map = Tacmach.project gl in 
-  let ty = mkArrow x (mkArrow x x) in 
-  let (em,x) = Evarutil.new_evar evar_map env  ty in 
+     
+let evar_binary (gl: goal_sigma) (x : constr) =
+  let env = Tacmach.pf_env gl in
+  let evar_map = Tacmach.project gl in
+  let ty = mkArrow x (mkArrow x x) in
+  let (em,x) = Evarutil.new_evar evar_map env  ty in
     x,( goal_update gl em)
 
-let evar_relation (gl: goal_sigma) (x: constr) = 
-  let env = Tacmach.pf_env gl in 
-  let evar_map = Tacmach.project gl in 
-  let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in 
-  let (em,r) = Evarutil.new_evar evar_map env  ty in 
+let evar_relation (gl: goal_sigma) (x: constr) =
+  let env = Tacmach.pf_env gl in
+  let evar_map = Tacmach.project gl in
+  let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
+  let (em,r) = Evarutil.new_evar evar_map env  ty in
     r,( goal_update gl em)
 
-let cps_evar_relation (x: constr) k = fun goal ->  
-  Tacmach.pf_apply 
-    (fun env em -> 
-      let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in 
+let cps_evar_relation (x: constr) k = fun goal -> 
+  Tacmach.pf_apply
+    (fun env em ->
+      let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
       let (em,r) = Evarutil.new_evar em env  ty in 	
       Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal
     )	goal
 
 (* decomp_term :  constr -> (constr, types) kind_of_term *)
 let decomp_term c = kind_of_term (strip_outer_cast c)
-    
+   
 let lapp c v  = mkApp (Lazy.force c, v)
 
 (** {2 Bindings with Coq' Standard Library}  *)
@@ -119,7 +119,7 @@ module Std = struct
 (* Here we package the module to be able to use List, later *)
 
 module Pair = struct
-  
+ 
   let path = ["Coq"; "Init"; "Datatypes"]
   let typ = lazy (init_constant path "prod")
   let pair = lazy (init_constant path "pair")
@@ -132,7 +132,7 @@ module Bool = struct
   let typ = lazy (init_constant path "bool")
   let ctrue = lazy (init_constant path "true")
   let cfalse = lazy (init_constant path "false")
-  let of_bool  b = 
+  let of_bool  b =
     if b then Lazy.force ctrue else Lazy.force cfalse
 end
 
@@ -157,13 +157,13 @@ module Option = struct
   let none = lazy (init_constant path "None")
   let some t x = mkApp (Lazy.force some, [| t ; x|])
   let none t = mkApp (Lazy.force none, [| t |])
-  let of_option t x = match x with 
+  let of_option t x = match x with
     | Some x -> some t x
     | None -> none t
-end    
+end   
 
 module Pos = struct
-    
+   
     let path = ["Coq" ; "NArith"; "BinPos"]
     let typ = lazy (init_constant path "positive")
     let xI =      lazy (init_constant path "xI")
@@ -172,14 +172,14 @@ module Pos = struct
 
     (* A coq positive from an int *)
     let of_int n =
-      let rec aux n = 
-	begin  match n with 
+      let rec aux n =
+	begin  match n with
 	  | n when n < 1 -> assert false
-	  | 1 -> Lazy.force xH 
-	  | n -> mkApp 
+	  | 1 -> Lazy.force xH
+	  | n -> mkApp
 	      (
-		(if n mod 2 = 0 
-		 then Lazy.force xO 
+		(if n mod 2 = 0
+		 then Lazy.force xO
 		 else Lazy.force xI
 		),  [| aux (n/2)|]
 	      )
@@ -187,7 +187,7 @@ module Pos = struct
       in
 	aux n
 end
-    
+   
 module Nat = struct
   let path = ["Coq" ; "Init"; "Datatypes"]
   let typ = lazy (init_constant path "nat")
@@ -195,11 +195,11 @@ module Nat = struct
   let _O =      lazy (init_constant  path "O")
     (* A coq nat from an int *)
   let of_int n =
-    let rec aux n = 
-      begin  match n with 
+    let rec aux n =
+      begin  match n with
 	| n when n < 0 -> assert false
 	| 0 -> Lazy.force _O
-	| n -> mkApp 
+	| n -> mkApp
 	    (
 	      (Lazy.force _S
 	      ),  [| aux (n-1)|]
@@ -208,24 +208,24 @@ module Nat = struct
     in
       aux n
 end
-    
+   
 (** Lists from the standard library*)
 module List = struct
   let path = ["Coq"; "Lists"; "List"]
   let typ = lazy (init_constant path "list")
   let nil = lazy (init_constant path "nil")
   let cons = lazy (init_constant path "cons")
-  let cons ty h t = 
+  let cons ty h t =
     mkApp (Lazy.force cons, [|  ty; h ; t |])
-  let nil ty = 
-    (mkApp (Lazy.force nil, [|  ty |])) 
-  let rec of_list ty = function 
+  let nil ty =
+    (mkApp (Lazy.force nil, [|  ty |]))
+  let rec of_list ty = function
     | [] -> nil ty
     | t::q -> cons ty t (of_list  ty q)
   let type_of_list ty =
     mkApp (Lazy.force typ, [|ty|])
 end
-    
+   
 (** Morphisms *)
 module Classes =
 struct
@@ -263,7 +263,7 @@ module Relation = struct
   let make ty r = {carrier = ty; r = r }
   let split t = t.carrier, t.r
 end
-    
+   
 module Transitive = struct
   type t =
       {
@@ -272,19 +272,19 @@ module Transitive = struct
 	transitive : constr;
       }
   let make ty leq transitive = {carrier = ty; leq = leq; transitive = transitive}
-  let infer goal ty leq  = 
-    let ask = Classes.mk_transitive ty leq in 
-    let transitive , goal = resolve_one_typeclass goal ask in 
-      make ty leq transitive, goal 
+  let infer goal ty leq  =
+    let ask = Classes.mk_transitive ty leq in
+    let transitive , goal = resolve_one_typeclass goal ask in
+      make ty leq transitive, goal
   let from_relation goal rlt =
     infer goal (rlt.Relation.carrier) (rlt.Relation.r)
   let cps_from_relation rlt k =
-    let ty =rlt.Relation.carrier in 
-    let r = rlt.Relation.r in 
-    let ask = Classes.mk_transitive  ty r in 
-    cps_resolve_one_typeclass ask 
+    let ty =rlt.Relation.carrier in
+    let r = rlt.Relation.r in
+    let ask = Classes.mk_transitive  ty r in
+    cps_resolve_one_typeclass ask
       (fun trans -> k (make ty r trans) )
-  let to_relation t = 
+  let to_relation t =
     {Relation.carrier = t.carrier; Relation.r = t.leq}
 
 end
@@ -297,55 +297,55 @@ module Equivalence = struct
 	equivalence : constr;	
       }
   let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence}
-  let infer goal ty eq  = 
-    let ask = Classes.mk_equivalence ty eq in 
-    let equivalence , goal = resolve_one_typeclass goal ask in 
-      make ty eq equivalence, goal 	  
+  let infer goal ty eq  =
+    let ask = Classes.mk_equivalence ty eq in
+    let equivalence , goal = resolve_one_typeclass goal ask in
+      make ty eq equivalence, goal 	 
   let from_relation goal rlt =
     infer goal (rlt.Relation.carrier) (rlt.Relation.r)
   let cps_from_relation rlt k =
-    let ty =rlt.Relation.carrier in 
-    let r = rlt.Relation.r in 
-    let ask = Classes.mk_equivalence  ty r in 
+    let ty =rlt.Relation.carrier in
+    let r = rlt.Relation.r in
+    let ask = Classes.mk_equivalence  ty r in
     cps_resolve_one_typeclass ask (fun equiv -> k (make ty r equiv) )
-  let to_relation t = 
+  let to_relation t =
     {Relation.carrier = t.carrier; Relation.r = t.eq}
   let split t =
     t.carrier, t.eq, t.equivalence
 end
-end 
+end
 (**[ match_as_equation goal eqt] see [eqt] as an equation. An
    optionnal rel_context can be provided to ensure taht the term
    remains typable*)
-let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option  = 
-  let env = Tacmach.pf_env goal in 
-  let env =  Environ.push_rel_context context env in 
-  let evar_map = Tacmach.project goal in 
+let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option  =
+  let env = Tacmach.pf_env goal in
+  let env =  Environ.push_rel_context context env in
+  let evar_map = Tacmach.project goal in
   begin
-    match decomp_term equation with 
+    match decomp_term equation with
       | App(c,ca) when Array.length ca >= 2 ->
-	let n = Array.length ca  in 
-	let left  =  ca.(n-2) in 
+	let n = Array.length ca  in
+	let left  =  ca.(n-2) in
 	let right =  ca.(n-1) in
-	let r = (mkApp (c, Array.sub ca 0 (n - 2))) in 
-	let carrier =  Typing.type_of env evar_map left in 
+	let r = (mkApp (c, Array.sub ca 0 (n - 2))) in
+	let carrier =  Typing.type_of env evar_map left in
 	let rlt =Std.Relation.make carrier r
-	in 
+	in
 	Some (left, right, rlt )
       | _ -> None
-  end 
+  end
 
 
 (** {1 Tacticals}  *)
 
 let tclTIME msg tac = fun gl ->
-  let u = Sys.time () in 
-  let r = tac gl in 
-  let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-.  u))) in 
+  let u = Sys.time () in
+  let r = tac gl in
+  let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-.  u))) in
     r
 
 let tclDEBUG msg tac = fun gl ->
-  let _ = Pp.msgnl (Pp.str msg) in 
+  let _ = Pp.msgnl (Pp.str msg) in
     tac gl
 
 let tclPRINT  tac = fun gl ->
@@ -356,24 +356,24 @@ let tclPRINT  tac = fun gl ->
 (** {1 Error related mechanisms}  *)
 (* functions to handle the failures of our tactic. Some should be
    reported [anomaly], some are on behalf of the user [user_error]*)
-let anomaly msg = 
+let anomaly msg =
   Util.anomaly ("[aac_tactics] " ^ msg)
 
-let user_error msg = 
+let user_error msg =
   Util.error ("[aac_tactics] " ^ msg)
 
 let warning msg =
   Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
 
-      
+     
 (** {1 Rewriting tactics used in aac_rewrite}  *)
 module Rewrite = struct
 (** Some informations about the hypothesis, with an (informal)
-    invariant: 
+    invariant:
     - [typeof hyp = hyptype]
     - [hyptype = forall context, body]
     - [body = rel left right]
-  
+ 
 *)
 
 type hypinfo =
@@ -389,24 +389,24 @@ type hypinfo =
     }
 
 let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proof_type.tactic = fun goal ->
-  let ctype =  Tacmach.pf_type_of goal c in  
-  let (rel_context, body_type) = Term.decompose_prod_assum ctype in  
+  let ctype =  Tacmach.pf_type_of goal c in 
+  let (rel_context, body_type) = Term.decompose_prod_assum ctype in 
   let rec check f e =
     match decomp_term e with
-      | Term.Rel i -> 
-	    let name, constr_option, types = Term.lookup_rel i rel_context 
+      | Term.Rel i ->
+	    let name, constr_option, types = Term.lookup_rel i rel_context
 	    in f types
       | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e
-  in 
-  begin match check_type with 
+  in
+  begin match check_type with
     | None -> ()
-    | Some f -> 
-      if not (check f body_type) 
+    | Some f ->
+      if not (check f body_type)
       then user_error "Unable to deal with higher-order or heterogeneous patterns";
   end;
-  begin 
+  begin
     match match_as_equation ~context:rel_context  goal body_type with
-      | None ->  
+      | None -> 
 	user_error "The hypothesis is not an applied relation"
       |  Some (hleft,hright,hrlt) ->
 	k {
@@ -417,11 +417,11 @@ let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proo
     	  context = rel_context;
     	  rel = hrlt ;
     	  left =hleft;
-    	  right = hright; 
+    	  right = hright;
 	}
 	goal
   end
-    
+   
 
 (* The problem : Given a term to rewrite of type [H :forall xn ... x1,
    t], we have to instanciate the subset of [xi] of type
@@ -438,75 +438,75 @@ let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proo
 
 (* Fresh evars for everyone (should be the good way to do this
    recompose in Coq v8.4) *)
-let recompose_prod  
+let recompose_prod 
     (context : Term.rel_context)
-    (subst : (int * Term.constr) list) 
+    (subst : (int * Term.constr) list)
     env
     em
     : Evd.evar_map * Term.constr list =
   (* the last index of rel relevant for the rewriting *)
-  let min_n = List.fold_left 
-    (fun acc (x,_) -> min acc x) 
-    (List.length context) subst in  
-  let rec aux context acc em n = 
-    let _ = Printf.printf "%i\n%!" n in 
-    match context with 
+  let min_n = List.fold_left
+    (fun acc (x,_) -> min acc x)
+    (List.length context) subst in 
+  let rec aux context acc em n =
+    let _ = Printf.printf "%i\n%!" n in
+    match context with
       | [] ->
 	env, em, acc
-      | ((name,c,ty) as t)::q -> 
+      | ((name,c,ty) as t)::q ->
 	let env, em, acc = aux q acc em (n+1) in
-	if n >= min_n 
+	if n >= min_n
 	then
-	  let em,x = 
-	    try em, List.assoc n subst 
-	    with | Not_found -> 
-	      Evarutil.new_evar em env (Term.substl acc ty) 
-	  in 
+	  let em,x =
+	    try em, List.assoc n subst
+	    with | Not_found ->
+	      Evarutil.new_evar em env (Term.substl acc ty)
+	  in
 	  (Environ.push_rel t env), em,x::acc
 	else
 	  env,em,acc
   in
-  let _,em,acc = aux context [] em 1 in 
-  em, acc 
+  let _,em,acc = aux context [] em 1 in
+  em, acc
 
 (* no fresh evars : instead, use a lambda abstraction around an
    application to handle non-instanciated variables. *)
-    
-let recompose_prod' 
+   
+let recompose_prod'
     (context : Term.rel_context)
     (subst : (int *Term.constr) list)
     c
     =
-  let rec popn pop n l = 
-    if n <= 0 then l 
-    else match l with 
+  let rec popn pop n l =
+    if n <= 0 then l
+    else match l with
       | [] -> []
       | t::q -> pop t :: (popn pop (n-1) q)
-  in 
-  let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in 
+  in
+  let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in
   let rec aux sign n next app ctxt =
-    match sign with 
-      | [] -> List.rev app, List.rev ctxt 
+    match sign with
+      | [] -> List.rev app, List.rev ctxt
       | decl::sign ->
-	try let term =  (List.assoc n subst) in 
+	try let term =  (List.assoc n subst) in
 	    aux sign (n+1) next (term::app) (None :: ctxt)
 	with
-	  | Not_found -> 
-	    let term = Term.mkRel next in 
+	  | Not_found ->
+	    let term = Term.mkRel next in
 	    aux sign (n+1) (next+1) (term::app) (Some decl :: ctxt)
-  in 
-  let app,ctxt = aux context 1 1 [] [] in 
+  in
+  let app,ctxt = aux context 1 1 [] [] in
   (* substitutes in the context *)
   let rec update ctxt app =
-    match ctxt,app with 
+    match ctxt,app with
       | [],_ -> []
       | _,[] -> []
       | None :: sign, _ :: app ->
 	None ::	update sign (List.map (Termops.pop) app)
-      | Some decl :: sign, _ :: app -> 
-	Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app)  
-  in 
-  let ctxt = update ctxt app in 
+      | Some decl :: sign, _ :: app ->
+	Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) 
+  in
+  let ctxt = update ctxt app in
   (* updates the rel accordingly, taking some care not to go to far
      beyond: it is important not to lift indexes homogeneously, we
      have to update *)
@@ -519,68 +519,68 @@ let recompose_prod'
   	update sign (decl :: res) (n+1)
   in
   let ctxt = update ctxt [] 0 in
-  let c = Term.applistc c (List.rev app) in 
-  let c = Term.it_mkLambda_or_LetIn c (ctxt) in 
+  let c = Term.applistc c (List.rev app) in
+  let c = Term.it_mkLambda_or_LetIn c (ctxt) in
   c
 
 (* Version de Matthieu
-let subst_rel_context k cstr ctx = 
+let subst_rel_context k cstr ctx =
   let (_, ctx') =
     List.fold_left (fun (k, ctx') (id, b, t) -> (succ k, (id, Option.map
       (Term.substnl [cstr] k) b, Term.substnl [cstr] k t) :: ctx')) (k, [])
       ctx in List.rev ctx'
 
-let recompose_prod' context subst c = 
+let recompose_prod' context subst c =
   let len = List.length context in
-  let rec aux sign n next app ctxt = 
-    match sign with 
-    | [] -> List.rev app, List.rev ctxt 
+  let rec aux sign n next app ctxt =
+    match sign with
+    | [] -> List.rev app, List.rev ctxt
     | decl::sign ->
-	try let term = (List.assoc n subst) in 
-	  aux (subst_rel_context 0 term sign) (pred n) (succ next) 
-	    (term::List.map (Term.lift (-1)) app) ctxt 
-	with Not_found -> 
-	  let term = Term.mkRel (len - next) in 
-	    aux sign (pred n) (succ next) (term::app) (decl :: ctxt) 
+	try let term = (List.assoc n subst) in
+	  aux (subst_rel_context 0 term sign) (pred n) (succ next)
+	    (term::List.map (Term.lift (-1)) app) ctxt
+	with Not_found ->
+	  let term = Term.mkRel (len - next) in
+	    aux sign (pred n) (succ next) (term::app) (decl :: ctxt)
   in
-  let app,ctxt = aux (List.rev context) len 0 [] [] in 
+  let app,ctxt = aux (List.rev context) len 0 [] [] in
     Term.it_mkLambda_or_LetIn (Term.applistc c(app)) (List.rev ctxt)
 *)
 
-let build 
-    (h : hypinfo) 
+let build
+    (h : hypinfo)
     (subst : (int *Term.constr) list)
-    (k :Term.constr -> Proof_type.tactic) 
+    (k :Term.constr -> Proof_type.tactic)
     : Proof_type.tactic = fun goal ->
-      let c = recompose_prod' h.context subst h.hyp in 
+      let c = recompose_prod' h.context subst h.hyp in
       Tacticals.tclTHENLIST [k c] goal
 
-let build_with_evar 
-    (h : hypinfo) 
+let build_with_evar
+    (h : hypinfo)
     (subst : (int *Term.constr) list)
-    (k :Term.constr -> Proof_type.tactic) 
-    : Proof_type.tactic 
+    (k :Term.constr -> Proof_type.tactic)
+    : Proof_type.tactic
     = fun goal ->
-      Tacmach.pf_apply 
-	(fun env em -> 
+      Tacmach.pf_apply
+	(fun env em ->
 	  let evar_map,  acc = recompose_prod h.context subst env em in
 	  let c = Term.applistc h.hyp (List.rev acc) in
 	  Tacticals.tclTHENLIST [Refiner.tclEVARS evar_map; k c] goal
-	) goal 
+	) goal
 
 
-let rewrite ?(abort=false)hypinfo subst k = 
-  build hypinfo subst 
-    (fun rew -> 
+let rewrite ?(abort=false)hypinfo subst k =
+  build hypinfo subst
+    (fun rew ->
       let tac =
 	if not abort then
 	  Equality.general_rewrite_bindings
-	    hypinfo.l2r 
-	    Termops.all_occurrences 
+	    hypinfo.l2r
+	    Termops.all_occurrences
 	    false
 	    (rew,Rawterm.NoBindings)
 	    true
-	else 
+	else
 	  Tacticals.tclIDTAC
       in k tac
     )