From 32170384190168856efeac5bcf90edf1170b54d6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 May 2002 10:48:37 +0000
Subject: Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques
 et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4606734fea..6da58adbc8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,3 +477,10 @@ let infer_local_decls env decls =
       push_rel d env, add_rel_decl d l, Constraint.union cst1 cst2
   | [] -> env, empty_rel_context, Constraint.empty in
   inferec env decls
+
+(* Exported typing functions *)
+
+let typing env c = 
+  let (j,cst) = infer env c in
+  let _ = add_constraints cst env in
+  j
-- 
cgit v1.2.3