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

4 files changed, 21 insertions, 0 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 597505686d..cf5a58eea4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -122,6 +122,7 @@ let pr_rawsort = function
 let pr_id = pr_id
 let pr_name = pr_name
 let pr_qualid = pr_qualid
+let pr_patvar = pr_id
 
 let pr_expl_args pr (a,expl) =
   match expl with
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 2becdbcfd6..afa744a507 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -46,6 +46,7 @@ val pr_sep_com :
 val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
 
 val pr_with_occurrences :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d3c4ae63da..61f7e377a2 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -57,6 +57,19 @@ let pr_constr t = pr_constr_env (Global.env()) t
 let pr_open_lconstr (_,c) = pr_lconstr c
 let pr_open_constr (_,c) = pr_constr c
 
+let pr_constr_under_binders_env_gen pr env (ids,c) =
+  (* Warning: clashes can occur with variables of same name in env but *)
+  (* we also need to preserve the actual names of the patterns *)
+  (* So what to do? *)
+  let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+  pr (push_rels_assum assums env) c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
+let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
+
 let pr_type_core at_top env t =
   pr_constr_expr (extern_type at_top env t)
 let pr_ltype_core at_top env t =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 52a0900759..241650b7d6 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -38,6 +38,12 @@ val pr_open_constr         : open_constr -> std_ppcmds
 val pr_open_lconstr_env    : env -> open_constr -> std_ppcmds
 val pr_open_lconstr        : open_constr -> std_ppcmds
 
+val pr_constr_under_binders_env  : env -> constr_under_binders -> std_ppcmds
+val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+
+val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+
 val pr_ltype_env_at_top    : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds