diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-17 13:30:50 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-17 13:56:14 +0100 |
| commit | f24543a02db80e2c4ab3065564fabb9b7d485a2f (patch) | |
| tree | 84cb3195743ae51d7bfe205e266373250c9e4616 /kernel/reduction.ml | |
| parent | d2f0997b7fddf3aa2f738e016d41663bf6595f61 (diff) | |
ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index de124299b..bf2ee2707 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb l2r evars env univs t1 t2 = +let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs @@ -627,7 +627,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = in if b then () else - let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in + let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in () (* Profiling *) @@ -644,7 +644,7 @@ let conv_leq = gen_conv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = - clos_fconv reds cv_pb l2r evars env univs t1 t2 + clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in s let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = @@ -655,7 +655,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = if b then cstrs else let univs = ((univs, Univ.Constraint.empty), inferred_universes) in - let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in + let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in cstrs (* Profiling *) |