From 74f6dceaab0146085e8ac48f9976665026099555 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 17:34:36 +0000
Subject: poursuite de Vernacentries

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0d2d5cba50..0824c192cf 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -937,3 +937,27 @@ let type_fixpoint env sigma lna lar vdefj =
       (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
   with IllBranch i ->
     error_ill_typed_rec_body CCI env i lna vdefj lar
+
+
+(* A function which checks that a term well typed verifies both
+   syntaxic conditions *)
+
+let control_only_guard env sigma = 
+  let rec control_rec = function
+    | Rel(p)        -> ()
+    | VAR _         -> ()
+    | DOP0(_)       -> ()
+    | DOPN(CoFix(_),cl) as cofix ->
+	check_cofix env sigma cofix; 
+	Array.iter control_rec cl
+    | DOPN(Fix(_),cl) as fix  -> 
+	check_fix env sigma fix; 
+        Array.iter control_rec cl
+    | DOPN(_,cl)    -> Array.iter control_rec cl
+    | DOPL(_,cl)    -> List.iter control_rec cl
+    | DOP1(_,c)     -> control_rec c
+    | DOP2(_,c1,c2) -> control_rec c1; control_rec c2
+    | DLAM(_,c)     -> control_rec c
+    | DLAMV(_,v)    -> Array.iter control_rec v
+  in 
+  control_rec 
-- 
cgit v1.2.3