diff options
| author | Hugo Herbelin | 2018-04-17 15:51:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | c2336868843bfe0c8e8a0b669641ca09814a45df (patch) | |
| tree | a7c72dd955484feb9217671a20d38f46571f01bc /pretyping | |
| parent | 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6 (diff) | |
Fixing an inconsistency in interpreting Ltac names linking to binder names.
The recursion names in fix and cofix were not renamed like other
binders were.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2d200ad27e..57a259b311 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -560,7 +560,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref | None -> () in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let _,newenv = push_rec_types !evdref (names,ftys) env in + let names,newenv = push_rec_types !evdref (names,ftys) env in let vdefj = Array.map2_i (fun i ctxt def -> |