From e08245e74ef52395052b926fc39d79e52f59af09 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 20 Aug 1999 15:00:59 +0000
Subject: machine: execute = typage avec univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@18 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 7d3b9f7ff4..2f7838b2d9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -56,8 +56,10 @@ type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
 
-type type_judgment = sorts judge
-type term_judgment = type_judgment judge
+type typed_type = sorts judge
+type typed_term = typed_type judge
+
+let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
 type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
 
@@ -1304,7 +1306,7 @@ let hcons_term (hast,hsorts,hsp,hname,hident,hstr) =
 module Htype =
   Hashcons.Make(
     struct
-      type t = type_judgment
+      type t = typed_type
       type u = (constr -> constr) * (sorts -> sorts)
       let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
       let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
-- 
cgit v1.2.3