diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 14:13:24 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 14:13:24 +0000 |
| commit | 0df14c3d0d2c71716bbed04451ad2e2541dcc6a3 (patch) | |
| tree | ec4918a0ef86b133860847f1b61e858b0920d6a1 /contrib/correctness/putil.ml | |
| parent | 2def0e4f8e5d075d815df253d316a96dd7257423 (diff) | |
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocamldep
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/putil.ml')
| -rw-r--r-- | contrib/correctness/putil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index 2f86d355e..e227a4459 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -264,7 +264,7 @@ and pp_binder = function let rec pp_cc_term = function CC_var id -> pr_id id - | CC_letin (_,_,bl,(c,_),c1) -> + | CC_letin (_,_,bl,c,c1) -> hOV 0 [< hOV 2 [< 'sTR"let "; prlist_with_sep (fun () -> [< 'sTR"," >]) (fun (id,_) -> pr_id id) bl; @@ -287,7 +287,7 @@ let rec pp_cc_term = function prlist_with_sep (fun () -> [< 'sTR","; 'cUT >]) pp_cc_term cl; 'sTR")" >] - | CC_case (_,(b,_),[e1;e2]) -> + | CC_case (_,b,[e1;e2]) -> hOV 0 [< 'sTR"if "; pp_cc_term b; 'sTR" then"; 'fNL; 'sTR" "; hOV 0 (pp_cc_term e1); 'fNL; 'sTR"else"; 'fNL; |