diff options
| author | Pierre-Marie Pédrot | 2019-07-31 13:32:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-31 14:35:23 +0200 |
| commit | fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 (patch) | |
| tree | 309674e4e3debf44ca7c10b07e429f75022c9dd6 /vernac/classes.ml | |
| parent | 162eefb562aca2c3741ec24d201deb881663e05a (diff) | |
Specialize the section API.
We split the function used to retrieve the local context from the one used to
provide the implicit status of each binder. Most of the users only rely on the
former indeed.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index efe452d5f1..075d89d0df 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -179,7 +179,7 @@ let discharge_class (_,cl) = let open CVars in let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right - ( fun (decl,_) (ctx', subst) -> + ( fun decl (ctx', subst) -> let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in |