Added support for Ltac-matching terms with variables bound in the pattern

- Instances found by matching.ml now collect the set of bound
  variables they possibly depend on in the pattern (see type
  Pattern.extended_patvar_map); the variables names are canonically
  ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
  tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
  is that we may have to re-type several times the same term but it is
  necessary for considering terms with locally bound variables of which
  we do not keep the type (and if even we had kept the type, we would have
  to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
  and I hope I did not break some intended existing behavior.

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

3 files changed, 17 insertions, 7 deletions

diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index f08ed7db6..4ea9c99b7 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -154,7 +154,7 @@ let field g =
       | _ -> raise Exit
     with Hipattern.NoEquationFound | Exit ->
       error "The statement is not built from Leibniz' equality" in
-  let th = VConstr (lookup (pf_env g) typ) in
+  let th = VConstr ([],lookup (pf_env g) typ) in
   (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
 
@@ -174,8 +174,8 @@ let field_term l g =
   Coqlib.check_required_library ["Coq";"field";"LegacyField"];
   let env = (pf_env g)
   and evc = (project g) in
-  let th = valueIn (VConstr (guess_theory env evc l))
-  and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
+  let th = valueIn (VConstr ([],guess_theory env evc l))
+  and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
   (List.fold_right
     (fun c a ->
      let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 0f8c2f010..4782e001a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -206,7 +206,7 @@ let exec_tactic env n f args =
   !res
 
 let constr_of = function
-  | VConstr c -> c
+  | VConstr ([],c) -> c
   | _ -> failwith "Ring.exec_tactic: anomaly"
 
 let stdlib_modules =
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 87c67cc14..80527f01d 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -105,14 +105,24 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
       else id
 
-  let pretype_id loc env (lvar,unbndltacvars) id =
+  let invert_ltac_bound_name env id0 id =
+    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    with Not_found ->
+      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+	str " depends on pattern variable name " ++ pr_id id ++
+	str " which is not bound in current context")
+
+  let pretype_id loc env sigma (lvar,unbndltacvars) id =
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
 	let (n,_,typ) = lookup_rel_id id (rel_context env) in
 	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
-	  List.assoc id lvar
+	  let (ids,c) = List.assoc id lvar in
+	  let subst = List.map (invert_ltac_bound_name env id) ids in
+	  let c = substl subst c in
+	  { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
 	with Not_found ->
 	  try
 	    let (_,_,typ) = lookup_named id env in
@@ -170,7 +180,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
     | RVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_id loc env lvar id)
+	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
     | REvar (loc, ev, instopt) ->