diff options
author | 2008-12-29 17:15:52 +0000 | |
---|---|---|
committer | 2008-12-29 17:15:52 +0000 | |
commit | b18a6d179903546cbf5745e601ab221f06e30078 (patch) | |
tree | c9ed543e785c2bcfad768669812778a9d3aea33e /parsing/ppconstr.ml | |
parent | f34f0420899594847b6e7633a4488f034a4300f6 (diff) |
- Added support for subterm matching in SearchAbout.
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
the naming of hypotheses (especially when doing "case H" with H of
type "{x|P<->Q}" since not unfolding will eventually introduce a name
"i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
of names manipulating type constr_pattern, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r-- | parsing/ppconstr.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index f5fe151ed..e16641a83 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -666,15 +666,15 @@ let rec strip_context n iscast t = type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds; - pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds } let default_term_pr = { pr_constr_expr = pr lsimple; pr_lconstr_expr = pr ltop; - pr_pattern_expr = pr lsimple; - pr_lpattern_expr = pr ltop + pr_constr_pattern_expr = pr lsimple; + pr_lconstr_pattern_expr = pr ltop } let term_pr = ref default_term_pr @@ -683,8 +683,8 @@ let set_term_pr = (:=) term_pr let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c -let pr_pattern_expr c = !term_pr.pr_pattern_expr c -let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c +let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c +let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c let pr_cases_pattern_expr = pr_patt ltop |