diff options
| author | Hugo Herbelin | 2015-11-22 17:17:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-22 21:17:25 +0100 |
| commit | af954522789043202d9c300a0bb37cbaf4958d60 (patch) | |
| tree | 7c8cfb9615c82ee3a78ff7f0f2e911dac4004f24 /pretyping | |
| parent | e583a79b5a0298fd08f34305cc876d5117913e95 (diff) | |
Fixing a bug of adjust_subst_to_rel_context.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5a55d47fd1..ebd9d939aa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -930,7 +930,7 @@ let adjust_subst_to_rel_context sign l = match sign, l with | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' | (_,Some c,_)::sign', args' -> - aux (substl (List.rev subst) c :: subst) sign' args' + aux (substl subst c :: subst) sign' args' | [], [] -> List.rev subst | _ -> anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l |