Cleaning up the type of Tacinterp.extract_ltac_constr_values.

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

3 files changed, 15 insertions, 13 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 64f8e208eb..ece0104b21 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -43,8 +43,8 @@ let instantiate n (ist,rawc) ido gl =
     let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
     let filtered = Evd.evar_filtered_env evi in
-    let ltac_vars = Tacinterp.extract_ltac_constr_values ist filtered in
-    let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
+    let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
+    let sigma' = w_refine (evk,evi) ((constrvars, ist.Geninterp.lfun),rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
         tclNORMEVAR
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7470de6c93..7158ddf7ed 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -401,14 +401,13 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
 
 (* Extract the constr list from lfun *)
 let extract_ltac_constr_values ist env =
-  let fold id v (vars1, vars2) =
+  let fold id v accu =
     try
       let c = coerce_to_constr env v in
-      (Id.Map.add id c vars1, vars2)
-    with CannotCoerceTo _ ->
-      (vars1, Id.Map.add id v vars2)
+      Id.Map.add id c accu
+    with CannotCoerceTo _ -> accu
   in
-  Id.Map.fold fold ist.lfun (Id.Map.empty, Id.Map.empty)
+  Id.Map.fold fold ist.lfun Id.Map.empty
 (** ppedrot: I have changed the semantics here. Before this patch, closure was
     implemented as a list and a variable could be bound several times with
     different types, resulting in its possible appearance on both sides. This
@@ -456,7 +455,8 @@ let interp_fresh_id ist env l =
 let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
-  let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
+  let constrvars = extract_ltac_constr_values ist env in
+  let vars = (constrvars, ist.lfun) in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -464,8 +464,8 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
        intros/lettac/inversion hypothesis names *)
   | Some c ->
       let fold id _ accu = id :: accu in
-      let ltacvars = Id.Map.fold fold ltacvars [] in
-      let ltacdata = (ltacvars, unbndltacvars) in
+      let ltacvars = Id.Map.fold fold constrvars [] in
+      let ltacdata = (ltacvars, ist.lfun) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
   let trace =
@@ -1315,7 +1315,7 @@ and interp_match_goal ist goal lz lr lmr =
 		       else mt()) ++ str"."))
     end in
     apply_match_goal ist env goal 0 lmr
-      (read_match_rule (fst (extract_ltac_constr_values ist env))
+      (read_match_rule (extract_ltac_constr_values ist env)
 	ist env (project goal) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
@@ -1519,7 +1519,7 @@ and interp_match ist g lz constr lmr =
           (fun () -> str "evaluation of the matched expression");
         raise reraise
   in
-  let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
+  let ilr = read_match_rule (extract_ltac_constr_values ist (pf_env g)) ist (pf_env g) sigma lmr in
   let res =
      try apply_match ist sigma csr ilr
      with reraise ->
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 407ad83b55..063104128c 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -45,7 +45,9 @@ val f_avoid_ids : Id.t list TacStore.field
 val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
-  Pretyping.ltac_var_map
+  Pattern.constr_under_binders Id.Map.t
+(** Given an interpretation signature, extract all values which are coercible to
+    a [constr]. *)
 
 (** Tactic extensions *)
 val add_tactic :