From 0b452cb010729f6e2d0f6400a8f823e5962407f0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 31 Jan 2007 08:39:53 +0000
Subject: Fix order of wf and measure arguments, patch Program doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing/ppvernac.ml')

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 807a3168c0..1b8123695d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -572,11 +572,11 @@ let rec pr_vernac = function
 			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
 			  else mt()
 		      | CWfRec c -> 
-			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
-			    pr_lconstr_expr c ++ str"}"
+			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ 
+			    pr_name name ++ str"}"
 		      | CMeasureRec c -> 
-			  spc() ++ str "{measure " ++ pr_name name ++ spc() ++ 
-			    pr_lconstr_expr c ++ str"}"
+			  spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ 
+			    pr_name name ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-- 
cgit v1.2.3