From ae7568b19bd9b19db153a9711ccf6a7e0e7caf6e Mon Sep 17 00:00:00 2001
From: Theo Zimmermann <theo.zimmermann@ens.fr>
Date: Tue, 16 Jun 2015 15:47:25 +0200
Subject: Add comments.

---
 tactics/rewrite.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6d26e91c6..b442ca98b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -631,13 +631,19 @@ let poly_inverse sort =
 
 type rewrite_proof = 
   | RewPrf of constr * constr
+  (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
   | RewCast of cast_kind
+  (** A proof of convertibility (with casts) *)
 
 type rewrite_result_info = {
   rew_car : constr;
+  (** A type *)
   rew_from : constr;
+  (** A term of type rew_car *)
   rew_to : constr;
+  (** A term of type rew_car *)
   rew_prf : rewrite_proof;
+  (** A proof of rew_from == rew_to *)
   rew_evars : evars;
 }
 
@@ -646,9 +652,14 @@ type rewrite_result =
 | Identity
 | Success of rewrite_result_info
 
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
-  (bool (* prop *) * constr option) -> evars -> 
-    'a * rewrite_result
+type 'a pure_strategy =
+  'a -> (* a parameter: for instance, a state *)
+  Environ.env ->
+  Id.t list -> (* Unfresh names *)
+  constr -> types -> (* first term and its type (convertible to rew_from) *)
+  (bool (* prop *) * constr option) ->
+  evars -> 
+  'a * rewrite_result (* the updated state for instance and the "result" *)
 
 type strategy = unit pure_strategy
 
-- 
cgit v1.2.3


From e9ddf697a1451f1928e05dba9722c876b6962e45 Mon Sep 17 00:00:00 2001
From: Theo Zimmermann <theo.zimmermann@ens.fr>
Date: Tue, 16 Jun 2015 18:50:58 +0200
Subject: Strategy is now a record type with a function field.

---
 tactics/rewrite.ml | 99 +++++++++++++++++++++++++++++++-----------------------
 1 file changed, 57 insertions(+), 42 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b442ca98b..fa9710ea3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -652,14 +652,14 @@ type rewrite_result =
 | Identity
 | Success of rewrite_result_info
 
-type 'a pure_strategy =
+type 'a pure_strategy = { strategy :
   'a -> (* a parameter: for instance, a state *)
   Environ.env ->
   Id.t list -> (* Unfresh names *)
   constr -> types -> (* first term and its type (convertible to rew_from) *)
   (bool (* prop *) * constr option) ->
   evars -> 
-  'a * rewrite_result (* the updated state for instance and the "result" *)
+  'a * rewrite_result (* the updated state for instance and the "result" *) }
 
 type strategy = unit pure_strategy
 
@@ -831,7 +831,7 @@ let apply_rule unify loccs : int pure_strategy =
     then List.mem occ occs 
     else not (List.mem occ occs) 
   in
-    fun occ env avoid t ty cstr evars ->
+    { strategy = fun occ env avoid t ty cstr evars ->
       let unif = if isEvar t then None else unify env evars t in
 	match unif with
 	| None -> (occ, Fail)
@@ -844,8 +844,9 @@ let apply_rule unify loccs : int pure_strategy =
               let rel, prf = get_rew_prf res in
 	      let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
               (occ, res)
+    }
 
-let apply_lemma l2r flags oc by loccs : strategy =
+let apply_lemma l2r flags oc by loccs : strategy = { strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
     let sigma, c = oc sigma in
     let sigma, hypinfo = decompose_applied_relation env sigma c in
@@ -858,8 +859,9 @@ let apply_lemma l2r flags oc by loccs : strategy =
       | None -> None
       | Some rew -> Some rew
     in
-    let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in
+    let _, res = (apply_rule unify loccs).strategy 0 env avoid t ty cstr evars in
     (), res
+						   }
 
 let e_app_poly env evars f args =
   let evars', c = app_poly_nocheck env !evars f args in
@@ -951,7 +953,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    state, (None :: acc, evars, progress)
 		  else
 		    let argty = Retyping.get_type_of env (goalevars evars) arg in
-		    let state, res = s state env avoid arg argty (prop,None) evars in
+		    let state, res = s.strategy state env avoid arg argty (prop,None) evars in
 		    let res' = 
 		      match res with
 		      | Identity ->
@@ -1003,7 +1005,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    evars, Some cstr', m, mty, args, Array.of_list args
 		  | None -> evars, None, m, mty, argsl, args
 	      in
-	      let state, m' = s state env avoid m mty (prop, cstr') evars in
+	      let state, m' = s.strategy state env avoid m mty (prop, cstr') evars in
 		match m' with
 		| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
 		| Identity -> rewrite_args state (Some false)
@@ -1110,7 +1112,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	let env' = Environ.push_rel (n', None, t) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
-	let state, b' = s state env' avoid b bty (prop, unlift env evars cstr) evars in
+	let state, b' = s.strategy state env' avoid b bty (prop, unlift env evars cstr) evars in
 	let res = 
 	  match b' with
 	  | Success r ->
@@ -1135,7 +1137,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	let cty = Retyping.get_type_of env (goalevars evars) c in
 	let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
 	let cstr' = Some eqty in
-	let state, c' = s state env avoid c cty (prop, cstr') evars' in
+	let state, c' = s.strategy state env avoid c cty (prop, cstr') evars' in
 	let state, res = 
 	  match c' with
 	  | Success r ->
@@ -1151,7 +1153,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		  if not (Option.is_empty found) then 
 		    (state, found, fun x -> lift 1 br :: acc x)
 		  else
-		    let state, res = s state env avoid br ty (prop,cstr) evars in
+		    let state, res = s.strategy state env avoid br ty (prop,cstr) evars in
 		      match res with
 		      | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
 		      | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1184,7 +1186,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	  | Fail | Identity -> res
 	in state, res
       | _ -> state, Fail
-  in aux
+  in { strategy = aux }
 
 let all_subterms = subterm true default_flags
 let one_subterm = subterm false default_flags
@@ -1195,7 +1197,7 @@ let one_subterm = subterm false default_flags
 let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) : 
     'a * rewrite_result =
   let state, nextres =
-    next state env avoid res.rew_to res.rew_car
+    next.strategy state env avoid res.rew_to res.rew_car
       (prop, get_opt_rew_rel res.rew_prf) res.rew_evars 
   in 
   let res = 
@@ -1232,15 +1234,17 @@ let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pur
 module Strategies =
   struct
 
-    let fail : 'a pure_strategy =
+    let fail : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
-	state, Fail
+      state, Fail
+				  }
 
-    let id : 'a pure_strategy =
+    let id : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars -> 
-	state, Identity
+      state, Identity
+				}
 
-    let refl : 'a pure_strategy =
+    let refl : 'a pure_strategy = { strategy =
       fun state env avoid t ty (prop,cstr) evars ->
 	let evars, rel = match cstr with
 	  | None -> 
@@ -1260,29 +1264,33 @@ module Strategies =
 	let res = Success { rew_car = ty; rew_from = t; rew_to = t;
 			       rew_prf = RewPrf (rel, proof); rew_evars = evars }
 	in state, res
+				  }
 
-    let progress (s : 'a pure_strategy) : 'a pure_strategy =
+    let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
-	let state, res = s state env avoid t ty cstr evars in
+	let state, res = s.strategy state env avoid t ty cstr evars in
 	  match res with
 	  | Fail -> state, Fail
 	  | Identity -> state, Fail
 	  | Success r -> state, Success r
+							     }
 	    
-    let seq first snd : 'a pure_strategy =
+    let seq first snd : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
-	let state, res = first state env avoid t ty cstr evars in
+	let state, res = first.strategy state env avoid t ty cstr evars in
 	  match res with
 	  | Fail -> state, Fail
-	  | Identity -> snd state env avoid t ty cstr evars
+	  | Identity -> snd.strategy state env avoid t ty cstr evars
 	  | Success res -> transitivity state env avoid (fst cstr) res snd
+					   }
 	    
-    let choice fst snd : 'a pure_strategy =
+    let choice fst snd : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
-	let state, res = fst state env avoid t ty cstr evars in
+	let state, res = fst.strategy state env avoid t ty cstr evars in
 	  match res with
-	  | Fail -> snd state env avoid t ty cstr evars
+	  | Fail -> snd.strategy state env avoid t ty cstr evars
 	  | Identity | Success _ -> state, res
+					    }
 
     let try_ str : 'a pure_strategy = choice str id
 
@@ -1291,7 +1299,8 @@ module Strategies =
       str s e l c t r ev
     
     let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
-      let rec aux state = f (fun state -> check_interrupt aux state) state in aux
+      let rec aux state = (f { strategy = fun state -> check_interrupt aux state }).strategy state in
+      { strategy = aux }
     
     let any (s : 'a pure_strategy) : 'a pure_strategy =
       fix (fun any -> try_ (seq s any))
@@ -1327,15 +1336,16 @@ module Strategies =
 	  (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
 				  hint.Autorewrite.rew_tac)) rules)
 
-    let hints (db : string) : 'a pure_strategy =
+    let hints (db : string) : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
       let rules = Autorewrite.find_matches db t in
       let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
 			hint.Autorewrite.rew_tac) in
       let lems = List.map lemma rules in
-	lemmas lems state env avoid t ty cstr evars
+      (lemmas lems).strategy state env avoid t ty cstr evars
+						 }
 
-    let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
+    let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
 	fun state env avoid t ty cstr evars ->
           let rfn, ckind = Redexpr.reduction_of_red_expr env r in
 	  let evars', t' = rfn env (goalevars evars) t in
@@ -1345,8 +1355,9 @@ module Strategies =
 	      state, Success { rew_car = ty; rew_from = t; rew_to = t';
 			       rew_prf = RewCast ckind; 
 			       rew_evars = evars', cstrevars evars }
+							   }
 	
-    let fold_glob c : 'a pure_strategy =
+    let fold_glob c : 'a pure_strategy = { strategy =
       fun state env avoid t ty cstr evars ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
 	let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
@@ -1362,6 +1373,7 @@ module Strategies =
 				  rew_prf = RewCast DEFAULTcast;
 				  rew_evars = (sigma, snd evars) }
 	  with e when Errors.noncritical e -> state, Fail
+					 }
   
 
 end
@@ -1372,7 +1384,7 @@ end
     even finding a first application of the rewriting lemma, in setoid_rewrite
     mode *)
 
-let rewrite_with l2r flags c occs : strategy =
+let rewrite_with l2r flags c occs : strategy = { strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
     let unify env evars t =
       let (sigma, cstrs) = evars in
@@ -1393,12 +1405,13 @@ let rewrite_with l2r flags c occs : strategy =
       Strategies.fix (fun aux -> 
 	Strategies.choice app (subterm true default_flags aux))
     in
-    let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in
-      ((), res)
+    let _, res = strat.strategy 0 env avoid t ty cstr (sigma, cstrs) in
+    ((), res)
+					       }
 
 let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
   let ty = Retyping.get_type_of env (goalevars evars) concl in
-  let _, res = s () env avoid concl ty (prop, Some cstr) evars in
+  let _, res = s.strategy () env avoid concl ty (prop, Some cstr) evars in
   res
 
 let solve_constraints env (evars,cstrs) =
@@ -1583,7 +1596,7 @@ let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars ->
     (sigma, (c, NoBindings))
   in
   let flags = general_rewrite_unif_flags () in
-  apply_lemma l2r flags c None occs () env avoid t ty cstr evars
+  (apply_lemma l2r flags c None occs).strategy () env avoid t ty cstr evars
 
 let interp_glob_constr_list env =
   let make c = (); fun sigma ->
@@ -1647,16 +1660,17 @@ let rec strategy_of_ast = function
       | Compose -> Strategies.seq
       | Choice -> Strategies.choice
     in f' s' t'
-  | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
+  | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
-  | StratTerms l -> 
+  | StratTerms l -> { strategy =
     (fun () env avoid t ty cstr evars ->
      let l' = interp_glob_constr_list env (List.map fst l) in
-       Strategies.lemmas l' () env avoid t ty cstr evars)
-  | StratEval r -> 
+     (Strategies.lemmas l').strategy () env avoid t ty cstr evars)
+		    }
+  | StratEval r -> { strategy =
     (fun () env avoid t ty cstr evars ->
      let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
-       Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
+       (Strategies.reduce r_interp).strategy () env avoid t ty cstr (sigma,cstrevars evars)) }
   | StratFold c -> Strategies.fold_glob (fst c)
 
 
@@ -1965,9 +1979,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
   let app = apply_rule unify occs in
   let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
   let substrat = Strategies.fix recstrat in
-  let strat () env avoid t ty cstr evars =
-    let _, res = substrat 0 env avoid t ty cstr evars in
+  let strat = { strategy = fun () env avoid t ty cstr evars ->
+    let _, res = substrat.strategy 0 env avoid t ty cstr evars in
     (), res
+	      }
   in
   let origsigma = project gl in
   init_setoid ();
-- 
cgit v1.2.3


From f3b553aa53c0dbff75bfc780209ebf33e35727fa Mon Sep 17 00:00:00 2001
From: Theo Zimmermann <theo.zimmermann@ens.fr>
Date: Fri, 19 Jun 2015 10:57:35 +0200
Subject: Put all arguments of strategy in record.

---
 tactics/rewrite.ml | 146 +++++++++++++++++++++++++++++++++--------------------
 1 file changed, 90 insertions(+), 56 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index fa9710ea3..db9a73f07 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -636,13 +636,13 @@ type rewrite_proof =
   (** A proof of convertibility (with casts) *)
 
 type rewrite_result_info = {
-  rew_car : constr;
+  rew_car : constr ;
   (** A type *)
-  rew_from : constr;
+  rew_from : constr ;
   (** A term of type rew_car *)
-  rew_to : constr;
+  rew_to : constr ;
   (** A term of type rew_car *)
-  rew_prf : rewrite_proof;
+  rew_prf : rewrite_proof ;
   (** A proof of rew_from == rew_to *)
   rew_evars : evars;
 }
@@ -652,14 +652,17 @@ type rewrite_result =
 | Identity
 | Success of rewrite_result_info
 
+type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
+			   env : Environ.env ;
+			   unfresh : Id.t list ; (* Unfresh names *)
+			   term1 : constr ;
+			   ty1 : types ; (* first term and its type (convertible to rew_from) *)
+			   cstr : (bool (* prop *) * constr option) ;
+			   evars : evars }
+	       
 type 'a pure_strategy = { strategy :
-  'a -> (* a parameter: for instance, a state *)
-  Environ.env ->
-  Id.t list -> (* Unfresh names *)
-  constr -> types -> (* first term and its type (convertible to rew_from) *)
-  (bool (* prop *) * constr option) ->
-  evars -> 
-  'a * rewrite_result (* the updated state for instance and the "result" *) }
+  'a strategy_input ->
+  'a * rewrite_result (* the updated state and the "result" *) }
 
 type strategy = unit pure_strategy
 
@@ -831,7 +834,8 @@ let apply_rule unify loccs : int pure_strategy =
     then List.mem occ occs 
     else not (List.mem occ occs) 
   in
-    { strategy = fun occ env avoid t ty cstr evars ->
+  { strategy = fun { state = occ ; env = env ; unfresh = avoid ;
+		     term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
       let unif = if isEvar t then None else unify env evars t in
 	match unif with
 	| None -> (occ, Fail)
@@ -847,7 +851,7 @@ let apply_rule unify loccs : int pure_strategy =
     }
 
 let apply_lemma l2r flags oc by loccs : strategy = { strategy =
-  fun () env avoid t ty cstr (sigma, cstrs) ->
+  fun ({ state = () ; env = env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
     let sigma, c = oc sigma in
     let sigma, hypinfo = decompose_applied_relation env sigma c in
     let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
@@ -859,7 +863,9 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
       | None -> None
       | Some rew -> Some rew
     in
-    let _, res = (apply_rule unify loccs).strategy 0 env avoid t ty cstr evars in
+    let _, res = (apply_rule unify loccs).strategy { input with
+						     state = 0 ;
+						     evars = evars } in
     (), res
 						   }
 
@@ -941,7 +947,8 @@ let unfold_match env sigma sk app =
 let is_rew_cast = function RewCast _ -> true | _ -> false
 
 let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
-  let rec aux state env avoid t ty (prop, cstr) evars =
+  let rec aux { state = state ; env = env ; unfresh = avoid ;
+		term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars = evars } =
     let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
       match kind_of_term t with
       | App (m, args) ->
@@ -953,7 +960,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    state, (None :: acc, evars, progress)
 		  else
 		    let argty = Retyping.get_type_of env (goalevars evars) arg in
-		    let state, res = s.strategy state env avoid arg argty (prop,None) evars in
+		    let state, res = s.strategy { state = state ; env = env ;
+						  unfresh = avoid ;
+						  term1 = arg ;	ty1 = argty ;
+						  cstr = (prop,None) ;
+						  evars = evars } in
 		    let res' = 
 		      match res with
 		      | Identity ->
@@ -1005,7 +1016,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    evars, Some cstr', m, mty, args, Array.of_list args
 		  | None -> evars, None, m, mty, argsl, args
 	      in
-	      let state, m' = s.strategy state env avoid m mty (prop, cstr') evars in
+	      let state, m' = s.strategy { state = state ; env = env ; unfresh = avoid ;
+					   term1 = m ; ty1 = mty ;
+					   cstr = (prop, cstr') ; evars = evars } in
 		match m' with
 		| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
 		| Identity -> rewrite_args state (Some false)
@@ -1042,7 +1055,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	    else TypeGlobal.arrow_morphism 
 	  in
 	  let (evars', mor), unfold = arr env evars tx tb x b in
-	  let state, res = aux state env avoid mor ty (prop,cstr) evars' in
+	  let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+				 term1 = mor ; ty1 = ty ;
+				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
 	    match res with
 	    | Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1072,7 +1087,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	      let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
 		(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
 	  in
-	  let state, res = aux state env avoid app ty (prop,cstr) evars' in
+	  let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+				 term1 = app ; ty1 = ty ;
+				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
 	    match res with
 	    | Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1112,7 +1129,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	let env' = Environ.push_rel (n', None, t) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
-	let state, b' = s.strategy state env' avoid b bty (prop, unlift env evars cstr) evars in
+	let state, b' = s.strategy { state = state ; env = env' ; unfresh = avoid ;
+				     term1 = b ; ty1 = bty ;
+				     cstr = (prop, unlift env evars cstr) ;
+				     evars = evars } in
 	let res = 
 	  match b' with
 	  | Success r ->
@@ -1137,7 +1157,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	let cty = Retyping.get_type_of env (goalevars evars) c in
 	let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
 	let cstr' = Some eqty in
-	let state, c' = s.strategy state env avoid c cty (prop, cstr') evars' in
+	let state, c' = s.strategy { state = state ; env = env ; unfresh = avoid ;
+				     term1 = c ; ty1 = cty ;
+				     cstr = (prop, cstr') ; evars = evars' } in
 	let state, res = 
 	  match c' with
 	  | Success r ->
@@ -1153,7 +1175,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		  if not (Option.is_empty found) then 
 		    (state, found, fun x -> lift 1 br :: acc x)
 		  else
-		    let state, res = s.strategy state env avoid br ty (prop,cstr) evars in
+		    let state, res = s.strategy { state = state ; env = env ; unfresh = avoid ;
+						  term1 = br ; ty1 = ty ;
+						  cstr = (prop,cstr) ; evars = evars } in
 		      match res with
 		      | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
 		      | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1168,7 +1192,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	      match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
 	      | None -> state, c'
 	      | Some (cst, _, t', eff (*FIXME*)) ->
-		let state, res = aux state env avoid t' ty (prop,cstr) evars in
+		 let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+					term1 = t' ; ty1 = ty ;
+					cstr = (prop,cstr) ; evars = evars } in
 		let res = 
 		  match res with
 		  | Success prf -> 
@@ -1197,8 +1223,10 @@ let one_subterm = subterm false default_flags
 let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) : 
     'a * rewrite_result =
   let state, nextres =
-    next.strategy state env avoid res.rew_to res.rew_car
-      (prop, get_opt_rew_rel res.rew_prf) res.rew_evars 
+    next.strategy { state = state ; env = env ; unfresh = avoid ;
+		    term1 = res.rew_to ; ty1 = res.rew_car ;
+		    cstr = (prop, get_opt_rew_rel res.rew_prf) ;
+		    evars = res.rew_evars }
   in 
   let res = 
     match nextres with
@@ -1235,17 +1263,20 @@ module Strategies =
   struct
 
     let fail : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
+      fun { state = state } ->
       state, Fail
 				  }
 
     let id : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars -> 
+      fun { state = state } -> 
       state, Identity
 				}
 
-    let refl : 'a pure_strategy = { strategy =
-      fun state env avoid t ty (prop,cstr) evars ->
+    let refl : 'a pure_strategy =
+      { strategy =
+	fun { state = state ; env = env ; unfresh = avoid ;
+	      term1 = t ; ty1 = ty ;
+	      cstr = (prop,cstr) ; evars = evars } ->
 	let evars, rel = match cstr with
 	  | None -> 
 	    let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
@@ -1267,8 +1298,8 @@ module Strategies =
 				  }
 
     let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
-	let state, res = s.strategy state env avoid t ty cstr evars in
+      fun input ->
+	let state, res = s.strategy input in
 	  match res with
 	  | Fail -> state, Fail
 	  | Identity -> state, Fail
@@ -1276,30 +1307,30 @@ module Strategies =
 							     }
 	    
     let seq first snd : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
-	let state, res = first.strategy state env avoid t ty cstr evars in
+      fun ({ env = env ; unfresh = avoid ; cstr = cstr } as input) ->
+	let state, res = first.strategy input in
 	  match res with
 	  | Fail -> state, Fail
-	  | Identity -> snd.strategy state env avoid t ty cstr evars
+	  | Identity -> snd.strategy { input with state = state }
 	  | Success res -> transitivity state env avoid (fst cstr) res snd
 					   }
 	    
     let choice fst snd : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
-	let state, res = fst.strategy state env avoid t ty cstr evars in
+      fun input ->
+	let state, res = fst.strategy input in
 	  match res with
-	  | Fail -> snd.strategy state env avoid t ty cstr evars
+	  | Fail -> snd.strategy { input with state = state }
 	  | Identity | Success _ -> state, res
 					    }
 
     let try_ str : 'a pure_strategy = choice str id
 
-    let check_interrupt str s e l c t r ev =
+    let check_interrupt str input =
       Control.check_for_interrupt ();
-      str s e l c t r ev
-    
+      str input
+
     let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
-      let rec aux state = (f { strategy = fun state -> check_interrupt aux state }).strategy state in
+      let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
       { strategy = aux }
     
     let any (s : 'a pure_strategy) : 'a pure_strategy =
@@ -1337,16 +1368,16 @@ module Strategies =
 				  hint.Autorewrite.rew_tac)) rules)
 
     let hints (db : string) : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
+      fun ({ term1 = t } as input) ->
       let rules = Autorewrite.find_matches db t in
       let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
 			hint.Autorewrite.rew_tac) in
       let lems = List.map lemma rules in
-      (lemmas lems).strategy state env avoid t ty cstr evars
+      (lemmas lems).strategy input
 						 }
 
     let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
-	fun state env avoid t ty cstr evars ->
+	fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
           let rfn, ckind = Redexpr.reduction_of_red_expr env r in
 	  let evars', t' = rfn env (goalevars evars) t in
 	    if eq_constr t' t then
@@ -1358,7 +1389,7 @@ module Strategies =
 							   }
 	
     let fold_glob c : 'a pure_strategy = { strategy =
-      fun state env avoid t ty cstr evars ->
+      fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
 	let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
 	let unfolded =
@@ -1385,7 +1416,7 @@ end
     mode *)
 
 let rewrite_with l2r flags c occs : strategy = { strategy =
-  fun () env avoid t ty cstr (sigma, cstrs) ->
+  fun ({ state = () } as input) ->
     let unify env evars t =
       let (sigma, cstrs) = evars in
       let ans =
@@ -1405,13 +1436,15 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
       Strategies.fix (fun aux -> 
 	Strategies.choice app (subterm true default_flags aux))
     in
-    let _, res = strat.strategy 0 env avoid t ty cstr (sigma, cstrs) in
+    let _, res = strat.strategy { input with state = 0 } in
     ((), res)
 					       }
 
 let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
   let ty = Retyping.get_type_of env (goalevars evars) concl in
-  let _, res = s.strategy () env avoid concl ty (prop, Some cstr) evars in
+  let _, res = s.strategy { state = () ; env = env ; unfresh = avoid ;
+			    term1 = concl ; ty1 = ty ;
+			    cstr = (prop, Some cstr) ; evars = evars } in
   res
 
 let solve_constraints env (evars,cstrs) =
@@ -1590,13 +1623,13 @@ let cl_rewrite_clause l left2right occs clause gl =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
     cl_rewrite_clause_strat strat clause gl
 
-let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars ->
+let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
   let c sigma =
     let (sigma, c) = Pretyping.understand_tcc env sigma c in
     (sigma, (c, NoBindings))
   in
   let flags = general_rewrite_unif_flags () in
-  (apply_lemma l2r flags c None occs).strategy () env avoid t ty cstr evars
+  (apply_lemma l2r flags c None occs).strategy input
 
 let interp_glob_constr_list env =
   let make c = (); fun sigma ->
@@ -1663,14 +1696,15 @@ let rec strategy_of_ast = function
   | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
   | StratTerms l -> { strategy =
-    (fun () env avoid t ty cstr evars ->
+    (fun ({ state = () ; env = env } as input) ->
      let l' = interp_glob_constr_list env (List.map fst l) in
-     (Strategies.lemmas l').strategy () env avoid t ty cstr evars)
+     (Strategies.lemmas l').strategy input)
 		    }
   | StratEval r -> { strategy =
-    (fun () env avoid t ty cstr evars ->
+    (fun ({ state = () ; env = env ; evars = evars } as input) ->
      let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
-       (Strategies.reduce r_interp).strategy () env avoid t ty cstr (sigma,cstrevars evars)) }
+     (Strategies.reduce r_interp).strategy { input with
+					     evars = (sigma,cstrevars evars) }) }
   | StratFold c -> Strategies.fold_glob (fst c)
 
 
@@ -1979,8 +2013,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
   let app = apply_rule unify occs in
   let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
   let substrat = Strategies.fix recstrat in
-  let strat = { strategy = fun () env avoid t ty cstr evars ->
-    let _, res = substrat.strategy 0 env avoid t ty cstr evars in
+  let strat = { strategy = fun ({ state = () } as input) ->
+    let _, res = substrat.strategy { input with state = 0 } in
     (), res
 	      }
   in
-- 
cgit v1.2.3


From 85fbcf9ed5c2f080e83f52fd2cd1791fb4172e74 Mon Sep 17 00:00:00 2001
From: Theo Zimmermann <theo.zimmermann@ens.fr>
Date: Fri, 19 Jun 2015 14:53:14 +0200
Subject: With the field record punning syntax.

---
 tactics/rewrite.ml | 94 ++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 49 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index db9a73f07..719cc7c98 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -834,8 +834,8 @@ let apply_rule unify loccs : int pure_strategy =
     then List.mem occ occs 
     else not (List.mem occ occs) 
   in
-  { strategy = fun { state = occ ; env = env ; unfresh = avoid ;
-		     term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
+  { strategy = fun { state = occ ; env ; unfresh ;
+		     term1 = t ; ty1 = ty ; cstr ; evars } ->
       let unif = if isEvar t then None else unify env evars t in
 	match unif with
 	| None -> (occ, Fail)
@@ -846,12 +846,12 @@ let apply_rule unify loccs : int pure_strategy =
 	    else
 	      let res = { rew with rew_car = ty } in
               let rel, prf = get_rew_prf res in
-	      let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
+	      let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
               (occ, res)
     }
 
 let apply_lemma l2r flags oc by loccs : strategy = { strategy =
-  fun ({ state = () ; env = env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
+  fun ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
     let sigma, c = oc sigma in
     let sigma, hypinfo = decompose_applied_relation env sigma c in
     let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
@@ -865,7 +865,7 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
     in
     let _, res = (apply_rule unify loccs).strategy { input with
 						     state = 0 ;
-						     evars = evars } in
+						     evars } in
     (), res
 						   }
 
@@ -947,8 +947,8 @@ let unfold_match env sigma sk app =
 let is_rew_cast = function RewCast _ -> true | _ -> false
 
 let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
-  let rec aux { state = state ; env = env ; unfresh = avoid ;
-		term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars = evars } =
+  let rec aux { state ; env ; unfresh ;
+		term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
     let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
       match kind_of_term t with
       | App (m, args) ->
@@ -960,11 +960,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    state, (None :: acc, evars, progress)
 		  else
 		    let argty = Retyping.get_type_of env (goalevars evars) arg in
-		    let state, res = s.strategy { state = state ; env = env ;
-						  unfresh = avoid ;
+		    let state, res = s.strategy { state ; env ;
+						  unfresh ;
 						  term1 = arg ;	ty1 = argty ;
 						  cstr = (prop,None) ;
-						  evars = evars } in
+						  evars } in
 		    let res' = 
 		      match res with
 		      | Identity ->
@@ -988,7 +988,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		      | Some r -> not (is_rew_cast r.rew_prf)) args'
 		  then
 		    let evars', prf, car, rel, c1, c2 = 
-		      resolve_morphism env avoid t m args args' (prop, cstr') evars' 
+		      resolve_morphism env unfresh t m args args' (prop, cstr') evars' 
 		    in
 		    let res = { rew_car = ty; rew_from = c1;
 				rew_to = c2; rew_prf = RewPrf (rel, prf);
@@ -1016,9 +1016,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    evars, Some cstr', m, mty, args, Array.of_list args
 		  | None -> evars, None, m, mty, argsl, args
 	      in
-	      let state, m' = s.strategy { state = state ; env = env ; unfresh = avoid ;
+	      let state, m' = s.strategy { state ; env ; unfresh ;
 					   term1 = m ; ty1 = mty ;
-					   cstr = (prop, cstr') ; evars = evars } in
+					   cstr = (prop, cstr') ; evars } in
 		match m' with
 		| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
 		| Identity -> rewrite_args state (Some false)
@@ -1041,7 +1041,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    let res = 
 		      match prf with
 		      | RewPrf (rel, prf) ->
-			Success (apply_constraint env avoid res.rew_car
+			Success (apply_constraint env unfresh res.rew_car
 				      rel prf (prop,cstr) res)
 		      | _ -> Success res
 		    in state, res
@@ -1055,7 +1055,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	    else TypeGlobal.arrow_morphism 
 	  in
 	  let (evars', mor), unfold = arr env evars tx tb x b in
-	  let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+	  let state, res = aux { state ; env ; unfresh ;
 				 term1 = mor ; ty1 = ty ;
 				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
@@ -1087,7 +1087,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	      let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
 		(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
 	  in
-	  let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+	  let state, res = aux { state ; env ; unfresh ;
 				 term1 = app ; ty1 = ty ;
 				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
@@ -1125,14 +1125,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       (* 	    | _ -> b') *)
 
       | Lambda (n, t, b) when flags.under_lambdas ->
-	let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
+	let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
 	let env' = Environ.push_rel (n', None, t) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
-	let state, b' = s.strategy { state = state ; env = env' ; unfresh = avoid ;
+	let state, b' = s.strategy { state ; env = env' ; unfresh ;
 				     term1 = b ; ty1 = bty ;
 				     cstr = (prop, unlift env evars cstr) ;
-				     evars = evars } in
+				     evars } in
 	let res = 
 	  match b' with
 	  | Success r ->
@@ -1157,7 +1157,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	let cty = Retyping.get_type_of env (goalevars evars) c in
 	let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
 	let cstr' = Some eqty in
-	let state, c' = s.strategy { state = state ; env = env ; unfresh = avoid ;
+	let state, c' = s.strategy { state ; env ; unfresh ;
 				     term1 = c ; ty1 = cty ;
 				     cstr = (prop, cstr') ; evars = evars' } in
 	let state, res = 
@@ -1165,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	  | Success r ->
 	    let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
 	    let res = make_leibniz_proof env case ty r in
-	      state, Success (coerce env avoid (prop,cstr) res)
+	      state, Success (coerce env unfresh (prop,cstr) res)
 	  | Fail | Identity ->
 	    if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
 	      let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1175,9 +1175,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		  if not (Option.is_empty found) then 
 		    (state, found, fun x -> lift 1 br :: acc x)
 		  else
-		    let state, res = s.strategy { state = state ; env = env ; unfresh = avoid ;
+		    let state, res = s.strategy { state ; env ; unfresh ;
 						  term1 = br ; ty1 = ty ;
-						  cstr = (prop,cstr) ; evars = evars } in
+						  cstr = (prop,cstr) ; evars } in
 		      match res with
 		      | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
 		      | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1192,9 +1192,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	      match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
 	      | None -> state, c'
 	      | Some (cst, _, t', eff (*FIXME*)) ->
-		 let state, res = aux { state = state ; env = env ; unfresh = avoid ;
+		 let state, res = aux { state ; env ; unfresh ;
 					term1 = t' ; ty1 = ty ;
-					cstr = (prop,cstr) ; evars = evars } in
+					cstr = (prop,cstr) ; evars } in
 		let res = 
 		  match res with
 		  | Success prf -> 
@@ -1208,7 +1208,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	  match res with
 	  | Success r ->  
 	    let rel, prf = get_rew_prf r in
-	      Success (apply_constraint env avoid r.rew_car rel prf (prop,cstr) r)
+	      Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
 	  | Fail | Identity -> res
 	in state, res
       | _ -> state, Fail
@@ -1220,10 +1220,10 @@ let one_subterm = subterm false default_flags
 (** Requires transitivity of the rewrite step, if not a reduction.
     Not tail-recursive. *)
 
-let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) : 
+let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) : 
     'a * rewrite_result =
   let state, nextres =
-    next.strategy { state = state ; env = env ; unfresh = avoid ;
+    next.strategy { state ; env ; unfresh ;
 		    term1 = res.rew_to ; ty1 = res.rew_car ;
 		    cstr = (prop, get_opt_rew_rel res.rew_prf) ;
 		    evars = res.rew_evars }
@@ -1262,21 +1262,17 @@ let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pur
 module Strategies =
   struct
 
-    let fail : 'a pure_strategy = { strategy =
-      fun { state = state } ->
-      state, Fail
-				  }
+    let fail : 'a pure_strategy =
+      { strategy = fun { state } -> state, Fail }
 
-    let id : 'a pure_strategy = { strategy =
-      fun { state = state } -> 
-      state, Identity
-				}
+    let id : 'a pure_strategy =
+      { strategy = fun { state } -> state, Identity }
 
     let refl : 'a pure_strategy =
       { strategy =
-	fun { state = state ; env = env ; unfresh = avoid ;
+	fun { state ; env ;
 	      term1 = t ; ty1 = ty ;
-	      cstr = (prop,cstr) ; evars = evars } ->
+	      cstr = (prop,cstr) ; evars } ->
 	let evars, rel = match cstr with
 	  | None -> 
 	    let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
@@ -1295,7 +1291,7 @@ module Strategies =
 	let res = Success { rew_car = ty; rew_from = t; rew_to = t;
 			       rew_prf = RewPrf (rel, proof); rew_evars = evars }
 	in state, res
-				  }
+      }
 
     let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
       fun input ->
@@ -1307,19 +1303,19 @@ module Strategies =
 							     }
 	    
     let seq first snd : 'a pure_strategy = { strategy =
-      fun ({ env = env ; unfresh = avoid ; cstr = cstr } as input) ->
+      fun ({ env ; unfresh ; cstr } as input) ->
 	let state, res = first.strategy input in
 	  match res with
 	  | Fail -> state, Fail
-	  | Identity -> snd.strategy { input with state = state }
-	  | Success res -> transitivity state env avoid (fst cstr) res snd
+	  | Identity -> snd.strategy { input with state }
+	  | Success res -> transitivity state env unfresh (fst cstr) res snd
 					   }
 	    
     let choice fst snd : 'a pure_strategy = { strategy =
       fun input ->
 	let state, res = fst.strategy input in
 	  match res with
-	  | Fail -> snd.strategy { input with state = state }
+	  | Fail -> snd.strategy { input with state }
 	  | Identity | Success _ -> state, res
 					    }
 
@@ -1389,7 +1385,7 @@ module Strategies =
 							   }
 	
     let fold_glob c : 'a pure_strategy = { strategy =
-      fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
+      fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
 	let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
 	let unfolded =
@@ -1440,11 +1436,11 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
     ((), res)
 					       }
 
-let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
+let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
   let ty = Retyping.get_type_of env (goalevars evars) concl in
-  let _, res = s.strategy { state = () ; env = env ; unfresh = avoid ;
+  let _, res = s.strategy { state = () ; env ; unfresh ;
 			    term1 = concl ; ty1 = ty ;
-			    cstr = (prop, Some cstr) ; evars = evars } in
+			    cstr = (prop, Some cstr) ; evars } in
   res
 
 let solve_constraints env (evars,cstrs) =
@@ -1696,12 +1692,12 @@ let rec strategy_of_ast = function
   | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
   | StratTerms l -> { strategy =
-    (fun ({ state = () ; env = env } as input) ->
+    (fun ({ state = () ; env } as input) ->
      let l' = interp_glob_constr_list env (List.map fst l) in
      (Strategies.lemmas l').strategy input)
 		    }
   | StratEval r -> { strategy =
-    (fun ({ state = () ; env = env ; evars = evars } as input) ->
+    (fun ({ state = () ; env ; evars } as input) ->
      let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
      (Strategies.reduce r_interp).strategy { input with
 					     evars = (sigma,cstrevars evars) }) }
-- 
cgit v1.2.3


From f39a711555d76926b6e0ddf5480a6411abc862a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 23 Jun 2015 16:59:08 +0200
Subject: Fixing incompatibility introduced with simpl in commit 364decf59c1
 (or maybe ca71714).

Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.

was working in 8.4 but was failing in 8.5beta2.

Note: Changes in tacintern.ml are otherwise purely cosmetic.
---
 tactics/tacintern.ml       | 12 ++++++------
 tactics/tacinterp.ml       | 14 +++++++++++++-
 test-suite/success/simpl.v |  7 +++++++
 3 files changed, 26 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d4c67b90f..fb22da83a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -341,7 +341,7 @@ let intern_typed_pattern ist p =
 
 let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
-    try l, Inl (intern_evaluable ist r)
+    try Inl (intern_evaluable ist r)
     with e when Logic.catchable_exception e ->
       (* Compatibility. In practice, this means that the code above
          is useless. Still the idea of having either an evaluable
@@ -356,19 +356,19 @@ let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let c = Constrintern.interp_reference sign r in
       match c with
       | GRef (_,r,None) ->
-          l, Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+          Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar (_,id) ->
           let r = evaluable_of_global_reference ist.genv (VarRef id) in
-          l, Inl (ArgArg (r,None))
+          Inl (ArgArg (r,None))
       | _ ->
-          l, Inr ((c,None),dummy_pat) in
-  match p with
+          Inr ((c,None),dummy_pat) in
+  (l, match p with
   | Inl r -> interp_ref r
   | Inr (CAppExpl(_,(None,r,None),[])) ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
-      l, Inr (intern_typed_pattern ist c)
+      Inr (intern_typed_pattern ist c))
 
 (* This seems fairly hacky, but it's the first way I've found to get proper
    globalization of [unfold].  --adamc *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 374c7c736..593e46b05 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -678,7 +678,19 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
-  | Inl b -> Inl (interp_evaluable ist env sigma b)
+  | Inl (ArgVar (loc,id)) ->
+      (* This is the encoding of an ltac var supposed to be bound
+         prioritary to an evaluable reference and otherwise to a constr
+         (it is an encoding to satisfy the "union" type given to Simpl) *)
+    let coerce_eval_ref_or_constr x =
+      try Inl (coerce_to_evaluable_ref env x)
+      with CannotCoerceTo _ ->
+        let c = coerce_to_closed_constr env x in
+        Inr (pi3 (pattern_of_constr env sigma c)) in
+    (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+     with Not_found ->
+       error_global_not_found_loc loc (qualid_of_ident id))
+  | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index e540ae5f3..5b87e877b 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
 simpl (unbox _ (unbox _ _)) at 2 4.
 match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
 Abort.
+
+(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
+
+Goal 2=1+1.
+match goal with |- (_ = ?c) => simpl c end.
+match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
+Abort.
-- 
cgit v1.2.3