* http://cs.unibo.it/helm/.
*)
+val meta: Cic.id -> Cic.annterm
+
+val hole: Cic.id -> Cic.annterm
+
val lift: int -> int -> Cic.annterm -> Cic.annterm
-val mk_ind:
- Cic.context -> Cic.id -> UriManager.uri -> int ->
- Cic.annterm -> Cic.annterm -> Cic.annterm list ->
- Cic.annterm option
+val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm
+
+val mk_pattern: int -> Cic.annterm -> Cic.annterm
+
+val get_clears:
+ Cic.context -> Cic.term -> (Cic.term * Cic.term) option ->
+ Cic.context * string list
+
+val clear: Cic.context -> string -> Cic.context
+
+val elim_inferred_type:
+ Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term