* the calculus *)
val whd: substitution -> Cic.context -> Cic.term -> Cic.term
+val are_convertible:
+ substitution -> Cic.context -> Cic.term -> Cic.term ->
+ bool
val type_of_aux':
- Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
+ Cic.metasenv -> substitution -> Cic.context -> Cic.term ->
+ Cic.term