Added {measure x f} as a valid recursion order.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 19 insertions, 11 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e73e88587b..a81ca599c8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -843,6 +843,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 and extern_recursion_order scopes vars = function
     RStructRec -> CStructRec
   | RWfRec c -> CWfRec (extern true scopes vars c)
+  | RMeasureRec c -> CMeasureRec (extern true scopes vars c)
 
 
 let extern_rawconstr vars c =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 57b5762d77..deb7abbde6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -775,17 +775,22 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
-	    let ro, ((ids',_,_),rbl) =
-	      (match order with
-		   CStructRec -> 
-		     RStructRec,
-		     List.fold_left intern_local_binder (env,[]) bl
-		 | CWfRec c -> 
-		     let before, after = list_chop (succ (out_some n)) bl in
-		     let ((ids',_,_),rafter) =
-		       List.fold_left intern_local_binder (env,[]) after in
-		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
-		       ro, List.fold_left intern_local_binder (env,rafter) before)
+	     let intern_ro_arg c f =
+	       let before, after = list_chop (succ (out_some n)) bl in
+	       let ((ids',_,_),rafter) =
+		 List.fold_left intern_local_binder (env,[]) after in
+	       let ro = (intern (ids', tmp_scope, scopes) c) in
+		 f ro, List.fold_left intern_local_binder (env,rafter) before
+	     in
+	     let ro, ((ids',_,_),rbl) =
+	       (match order with
+		    CStructRec -> 
+		      RStructRec,
+		      List.fold_left intern_local_binder (env,[]) bl
+		  | CWfRec c ->
+		      intern_ro_arg c (fun r -> RWfRec r)
+		  | CMeasureRec c ->
+		      intern_ro_arg c (fun r -> RMeasureRec r))
 	    in
 	    let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5b9b404425..6e7ea0f9c8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -544,6 +544,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 (***********************)
 (* For binders parsing *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 9173d3116e..57a2c976cb 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -122,6 +122,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr