assert false
in
let metasenv, subst, term, _ =
- NCicRefiner.typeof
+ NCicRefiner.typeof
+ (NCicUnifHint.db ())
~look_for_coercion:(
if use_coercions then
NCicCoercion.look_for_coercion coercion_db
NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
+
+ NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
+ NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
+ NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
+ NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
+ NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
+ NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
+
+ NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
+ NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
+ NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
+ NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
+ NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
+ NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
+
+ NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
+ NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
+
;;