(* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
+(* web interface stuff *)
+
+let logger =
+ ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
let type_t = typeof_aux context t in
if not (R.are_convertible ~subst ~metasenv context type_t ct) then
raise (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context: "^^
- "expected a term of type %s, found %s of type %s")
- (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context: "^^
+ "expected a term of type %s, found %s of type %s")
+ (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
) l lifted_canonical_context
with
Invalid_argument _ ->
returns_a_coinductive ~subst ((n,C.Decl so)::context) de
| _ -> None
-and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
-(* ALIAS typecheck *)
-(*
- let cobj,ugraph1 =
- match CicEnvironment.is_type_checked ~trust:true ugraph uri with
- CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj uobj ->
+and type_of_constant ref =
+assert false (*
+ let cobj =
+ match E.get_obj uri with
+ | true, cobj -> cobj
+ | false, uobj ->
logger#log (`Start_type_checking uri) ;
let ugraph1_dust =
typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in