diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 17:38:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 17:50:05 +0200 |
| commit | 116ec0eb91ce05d21433c1127636f2abf4ec55c4 (patch) | |
| tree | 8a278dbb972459c7016f531f87df272bdc298292 /kernel/context.ml | |
| parent | 26b6fa7fe182083112c7eff080f5130556a08678 (diff) | |
Removing an unused variant of Context.fold_named_context_reverse.
Diffstat (limited to 'kernel/context.ml')
0 files changed, 0 insertions, 0 deletions