* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception Bad_pattern of string Lazy.t
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
* @raise Bad_pattern
* *)
let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
- ~(pattern: (Cic.term, ProofEngineTypes.lazy_term) ProofEngineTypes.pattern)
+ ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
let find_pattern_for name =