diff options
| author | filliatr | 1999-08-20 15:00:59 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-20 15:00:59 +0000 |
| commit | e08245e74ef52395052b926fc39d79e52f59af09 (patch) | |
| tree | d6e428173c43e01c852505da13d9b744cccbb49d /kernel/term.ml | |
| parent | 10f4e87cca4f83700c9b6a8acffc081de66dc164 (diff) | |
machine: execute = typage avec univers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@18 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 8 |
1 files changed, 5 insertions, 3 deletions
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 |