From 098236cf193fb98d2990c6d52d53a4d4b3f72ba0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 22 Jun 2006 12:51:04 +0000
Subject: 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
---
 pretyping/rawterm.ml  | 2 +-
 pretyping/rawterm.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 9a0e51e108..78e616d98a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -73,7 +73,7 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index f6541ff314..c61c61b0f3 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -70,7 +70,7 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
-- 
cgit v1.2.3