From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 24 Jul 2015 08:46:09 +0200
Subject: Propagate `Guarded` flag from syntax to kernel.

The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
---
 kernel/fast_typeops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/fast_typeops.mli')

diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 90d9c55f16..98dbefad13 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -18,6 +18,6 @@ open Environ
  *)
 
 
-val infer      : env -> constr       -> unsafe_judgment
-val infer_v    : env -> constr array -> unsafe_judgment array
-val infer_type : env -> types        -> unsafe_type_judgment
+val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
+val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
+val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
-- 
cgit v1.2.3