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 | |
| parent | 26b6fa7fe182083112c7eff080f5130556a08678 (diff) | |
Removing an unused variant of Context.fold_named_context_reverse.
| -rw-r--r-- | pretyping/termops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 1e3d2e4e9..826104f59 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -62,9 +62,6 @@ val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr the context where the letins are expanded *) val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr -val it_named_context_quantifier : - (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a - (** {6 Generic iterators on constr} *) val map_constr_with_named_binders : |