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

4 files changed, 30 insertions, 9 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 723936f5b9..ea694f61d2 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -137,6 +137,21 @@ automatically generated by the pattern-matching compilation algorithm):
   Obligations.
 \end{coq_example}
 
+You can use a well-founded order or a measure as termination orders using the syntax:
+\begin{coq_eval}
+Reset Initial.
+Require Import Arith.
+\end{coq_eval}
+\begin{coq_example}
+Definition id (n : nat) := n.
+
+Program Fixpoint div2 (n : nat) {measure id n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
+  match n with
+  | S (S p) => S (div2 p)
+  | _ => O
+  end.
+\end{coq_example}
+
 \subsection{\tt Program Lemma {\ident} : type.
   \comindex{Program Lemma}
   \label{ProgramLemma}}
@@ -151,10 +166,16 @@ The following commands are available to manipulate obligations:
 \begin{itemize}
 \item {\tt Obligations [of \ident]} Displays all remaining
   obligations.
-\item {\tt Solve Obligation num [of \ident]} Start the proof of
+\item {\tt Next Obligation [of \ident]} Start the proof of the next
+  unsolved obligation.
+\item {\tt Obligation num [of \ident]} Start the proof of
   obligation {\tt num}.
 \item {\tt Solve Obligations [of \ident] using} {\tacexpr} Tries to solve
   each obligation using the given tactic.
+\item {\tt Admit Obligations [of \ident]} Admits all
+  obligations (does not work with structurally recursive programs).
+\item {\tt Obligations Tactic := \expr} Sets the default obligation
+  solving tactic applied to all obligations.
 \end{itemize}
   
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f097f7e6e..9a50eb897e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -231,8 +231,8 @@ GEXTEND Gram
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
-      | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
-      | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel)
+      | "{"; IDENT "wf"; rel=constr; id=name; "}" -> (Some id, CWfRec rel)
+      | "{"; IDENT "measure"; rel=constr; id=name; "}" -> (Some id, CMeasureRec rel)
       | ->  (None, CStructRec)
       ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d08a9b06c0..ad1e3abb78 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -266,8 +266,8 @@ GEXTEND Gram
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
-      | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
-      | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) 
+      | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
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_