* http://cs.unibo.it/helm/.
*)
+open Printf
+
exception Impossible of int;;
exception NotRefinable of string;;
exception Uncertain of string;;
CicMkImplicit.identity_relocation_list_for_metavariable context
in
C.Meta (idx, irl), subst, metasenv'
-(*
- raise
- (Uncertain
- ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
- CicPp.ppterm t2''))
-*)
| (_,_) ->
- raise
- (NotRefinable
- ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
+ raise (NotRefinable (sprintf
+ "Two types were expected, found %s of type %s and %s of type %s"
+ (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
+ (CicPp.ppterm t2'')))
and eat_prods subst metasenv context hetype =
function