* http://cs.unibo.it/helm/.
*)
+val metas_of_proof_time : float ref
+
type equality =
int * (* weight *)
proof * (* proof *)
val string_of_proof: proof -> string
+val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+
exception MatchingFailure
(** matching between two terms. Can raise MatchingFailure *)
val matching:
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
such case should be significantly faster than CicUnification.fo_unif
*)
val unification:
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
val string_of_equality: ?env:environment -> equality -> string
val metas_of_term: Cic.term -> int list
+val metas_of_proof: proof -> int list
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality