From 07e4438bd758c2ced8caf09a6961ccd77d84e42b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 19 Sep 2014 01:13:39 +0200
Subject: Revert change of e_contextually as it needlessly expands all
 primitive projections in the term.

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

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8875d1d936..39015d89a9 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -973,9 +973,9 @@ let e_contextually byhead (occs,c) f env sigma t =
       else
 	t
     with ConstrMatching.PatternMatchingFailure ->
-      Evarsolve.map_constr_with_binders_left_to_right 
+      map_constr_with_binders_left_to_right 
 	(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
-        traverse envc sigma t
+        traverse envc t
   in
   let t' = traverse (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-- 
cgit v1.2.3