diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /parsing/ppconstr.ml | |
| parent | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff) | |
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 8bf2f4207..a95fa4bad 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -374,13 +374,18 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c -let pr_fixdecl pr prd dangling_with_for (id,n,bl,t,c) = +let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = let annot = let ids = names_of_local_assums bl in - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" - else mt() in - pr_recursive_decl pr prd dangling_with_for id bl annot t c + match ro with + CStructRec -> + if List.length ids > 1 then + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" + else mt() + | CWfRec c -> + spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}" + in + pr_recursive_decl pr prd dangling_with_for id bl annot t c let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c |