From af954522789043202d9c300a0bb37cbaf4958d60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Nov 2015 17:17:49 +0100
Subject: Fixing a bug of adjust_subst_to_rel_context.

---
 pretyping/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3