diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 08bcd1ddd..1855858ca 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1137,6 +1137,7 @@ let nb_prod = let rec eq_constr m n = (m==n) or compare_constr eq_constr m n + let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) (*******************) @@ -1184,3 +1185,11 @@ let hcons_constr (hkn,hdir,hname,hident,hstr) = (hcci,htcci) let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names()) + + +(*******) +(* Type of abstract machine values *) +type values + + + |