From 221a2ee32545e22f8002b0903b215d8c890b2125 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Nov 2014 17:51:43 +0100
Subject: Fix resolve_morphism to build well-scoped terms in case some
 arguments of the function are dependent.

---
 tactics/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 68605119ca..49c0a81eb1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -819,14 +819,14 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
-		error "Cannot rewrite the argument of a dependent function";
+		error "Cannot rewrite inside dependent arguments of a function";
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
   in
   let proof = applistc proj (List.rev projargs) in
   let newt = applistc m' (List.rev typeargs) in
     match respars with
-	[ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt
+	[ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
       | _ -> assert(false)
 
 let apply_constraint env avoid car rel prf cstr res =
-- 
cgit v1.2.3