From 9a7f9eeb6e5388b56e575a60aeac87330744440c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 13:56:43 +0000
Subject: mise au point Declare et avancee dans Astterm

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@175 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typing.ml  | 3 +++
 pretyping/typing.mli | 2 ++
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c12f9bb34f..44af99e19f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -136,6 +136,9 @@ let safe_machine env sigma constr =
   let mf = { fix = false; nocheck = false } in
   execute mf env sigma constr
 
+let unsafe_machine env sigma constr =
+  let mf = { fix = false; nocheck = true } in
+  execute mf env sigma constr
 
 (* Type of a constr *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 80fcc5ec99..ee68e518f4 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -10,6 +10,8 @@ open Evd
 (* This module provides the typing machine with existential variables
    (but without universes). *)
 
+val unsafe_machine : env -> 'a evar_map -> constr -> unsafe_judgment
+
 val type_of : env -> 'a evar_map -> constr -> constr
 
 val execute_type : env -> 'a evar_map -> constr -> typed_type
-- 
cgit v1.2.3