From c3d45696c271df086c39488d8a86fd2b60ec8132 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 6 Jun 2010 14:04:29 +0000
Subject: 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
---
 parsing/ppconstr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing/ppconstr.mli')

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
-- 
cgit v1.2.3