diff options
| author | Pierre-Marie Pédrot | 2015-11-26 14:24:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-26 14:24:54 +0100 |
| commit | 36c6e9508a42d00686e90441999481354152aaa3 (patch) | |
| tree | 882909be1c393764f13923e059448f3808fa0966 /engine | |
| parent | b58e8aa6525d45473f88fbea71bab88a2b46c825 (diff) | |
| parent | b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 5a55d47fd1..ebd9d939aa 100644 --- a/engine/termops.ml +++ b/engine/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 |