-(* From now on we recreate a kernel abstraction where substitutions are part of
- * the calculus *)
-
-let lift subst n term =
-(* incr subst_counter; *)
- let term = apply_subst subst term in
- try
- CicSubstitution.lift n term
- with e ->
- raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
-
-let subst subst t1 t2 =
-(* incr subst_counter; *)
- let t1 = apply_subst subst t1 in
- let t2 = apply_subst subst t2 in
- try
- CicSubstitution.subst t1 t2
- with e ->
- raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
-
-let whd subst context term =
-(* incr whd_counter; *)
- let term = apply_subst subst term in
- let context = apply_subst_context subst context in
- try
- CicReduction.whd context term
- with e ->
- raise (MetaSubstFailure ("Weak head reduction failure: " ^
- Printexc.to_string e))
-
-let are_convertible subst context t1 t2 =
-(* incr are_convertible_counter; *)
- let context = apply_subst_context subst context in
- let t1 = apply_subst subst t1 in
- let t2 = apply_subst subst t2 in
- CicReduction.are_convertible context t1 t2
-