diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-24 17:35:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-24 17:42:14 +0200 |
| commit | 1556c6b8f77d16814ff1c53fb14fc9b06574ec4b (patch) | |
| tree | 7c3085729fea24ebf5b12d785da22e528e38174a /kernel/term_typing.ml | |
| parent | 08e87eb96ab67ead60d92394eec6066d9b52e55e (diff) | |
Remove an ununsed pattern and commented code in the kernel.
Reestablish completeness in conversion when Opaque primitive
projections are used.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8f41f356d..79b3d518a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -65,11 +65,6 @@ let handle_side_effects env body side_eff = | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> - (* let subst = *) - (* Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) *) - (* Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') *) - (* in *) - (* Vars.subst_univs_level_constr subst b *) Vars.subst_instance_constr u' b | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in let fix_body (c,cb,b) t = |