Move the specific map_constr_with_binders_left_to_right

for e_contextually where it is used. Bug #3648 is fixed.

5 files changed, 24 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 15b16a36bc..3b3c9f9eed 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -850,7 +850,7 @@ let apply_on_subterm env evdref f c t =
       | _ ->
         map_constr_with_binders_left_to_right
 	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
-	  applyrec acc !evdref t
+	  applyrec acc t
   in
   applyrec (env,(0,c)) t
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index e47fad81bb..ba877d35c8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,14 +101,6 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   in
     if !modified then !evdref, t' else !evdref, t
 
-let map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = 
-  match kind_of_term c with
-  | Proj (p, r) -> (* Treat specially for partial applications *)
-    let t = Retyping.expand_projection env sigma p r [] in
-      map_constr_with_binders_left_to_right g f	acc t
-  | _ -> map_constr_with_binders_left_to_right g f acc c
-      
-
 (************************)
 (* Unification results  *)
 (************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 86c9908c84..0d0f3c0e51 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,9 +69,3 @@ val check_evar_instance :
 
 val remove_instance_local_defs :
   evar_map -> existential_key -> constr array -> constr list
-
-(* This is up to partial applications and primitive projection expansion *)
-val map_constr_with_binders_left_to_right : 
-  (Context.rel_declaration -> (env * 'a) -> (env * 'a)) ->
-  ((env * 'a) -> constr -> constr) ->
-  (env * 'a) -> evar_map -> constr -> constr
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 44ff2b5b8c..01317ba253 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -150,8 +150,7 @@ let pattern_of_constr sigma t =
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
-    | Proj (p, c) ->  
-        PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
+    | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
     | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
           | Evar_kinds.MatchingVar (b,id) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f0d0d45267..6f6de95fcd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -945,6 +945,26 @@ let matches_head env sigma c t =
 
 let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
 
+(** FIXME: Specific function to handle projections: it ignores what happens on the
+    parameters. This is a temporary fix while rewrite etc... are not up to equivalence
+    of the projection and it's eta expanded form.
+*)
+let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = 
+  match kind_of_term c with
+  | Proj (p, r) -> (* Treat specially for partial applications *)
+    let t = Retyping.expand_projection env sigma p r [] in
+    let hdf, al = destApp t in
+    let a = al.(Array.length al - 1) in
+    let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
+    let app' = f acc app in
+    let a' = f acc a in
+    let hdf', al' = destApp app' in
+      if hdf' == hdf then
+        (* Still the same projection, we ignore the change in parameters *)
+	mkProj (p, a')
+      else mkApp (app', [| a' |])
+  | _ -> map_constr_with_binders_left_to_right g f acc c
+
 let e_contextually byhead (occs,c) f env sigma t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
@@ -977,9 +997,9 @@ let e_contextually byhead (occs,c) f env sigma t =
       else
 	t
     with ConstrMatching.PatternMatchingFailure ->
-      map_constr_with_binders_left_to_right 
+      change_map_constr_with_binders_left_to_right 
 	(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
-        traverse envc t
+        traverse envc sigma t
   in
   let t' = traverse (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;