diff options
| author | herbelin | 2009-06-06 21:34:37 +0000 |
|---|---|---|
| committer | herbelin | 2009-06-06 21:34:37 +0000 |
| commit | f1967c38371e3d9cd7c38623540e5191c7cd2d6e (patch) | |
| tree | 7110d004c26af9646f582d167a360e82946b3fb9 /parsing | |
| parent | 4ffffb89d777b1a298ca979025625a9149e7e8ac (diff) | |
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
instead of the index required by the user; extended FixRule and
Cofix accordingly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/printer.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 267d550a97..37083eb461 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -427,10 +427,11 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | FixRule (f,n,[]) -> + | FixRule (f,n,[],_) -> (str"fix " ++ pr_id f ++ str"/" ++ int n) - | FixRule (f,n,others) -> + | FixRule (f,n,others,j) -> + if j<>0 then warning "Unsupported printing of \"fix\""; let rec print_mut = function | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth @@ -438,10 +439,11 @@ let pr_prim_rule = function (str"fix " ++ pr_id f ++ str"/" ++ int n ++ str" with " ++ print_mut others) - | Cofix (f,[]) -> + | Cofix (f,[],_) -> (str"cofix " ++ pr_id f) - | Cofix (f,others) -> + | Cofix (f,others,j) -> + if j<>0 then warning "Unsupported printing of \"fix\""; let rec print_mut = function | (f,ar)::oth -> (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) |