diff options
| author | herbelin | 2009-12-24 11:05:43 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-24 11:05:43 +0000 |
| commit | fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa (patch) | |
| tree | b5a8aad89c9ea0a19d05be81d94e4a8d53c4ffe2 /parsing/ppvernac.ml | |
| parent | 3c3bbccb00cb1c13c28a052488fc2c5311d47298 (diff) | |
In "simpl c" and "change c with d", c can be a pattern.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 224b2e2bf9..3ef45072cc 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -69,7 +69,7 @@ let pr_gen env t = pr_raw_generic pr_constr_expr pr_lconstr_expr - (pr_raw_tactic_level env) pr_reference t + (pr_raw_tactic_level env) pr_constr_expr pr_reference t let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac @@ -579,7 +579,7 @@ let rec pr_vernac = function | None -> mt() | Some r -> str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global) r ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ str" in" ++ spc() in let pr_def_body = function | DefineBody (bl,red,body,d) -> @@ -890,7 +890,7 @@ let rec pr_vernac = function let pr_mayeval r c = match r with | Some r0 -> hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global) r0 ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) in |