Revert "Fixing #1225: we now skip the canonically built binding contexts of"

This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0.

Very sorry not ready.

3 files changed, 28 insertions, 71 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index c8d90fffea..95a6ba79db 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -14,8 +14,6 @@ open Locus
 open Term
 open Nameops
 open Termops
-open Environ
-open Inductiveops
 open Pretype_errors
 
 (** Processing occurrences *)
@@ -75,17 +73,6 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
       let acc,typ = f acc typ in
       acc,(id,Some body,typ)
 
-let rec process_under_binders f envk sign p =
-  let rec aux (env,k) sign p =
-    match (sign,kind_of_term p) with
-    | [], _ -> f (env,k) p
-    | (_,None,t as d)::sign, Lambda (na,_,p) ->
-      mkLambda (na,t,aux (push_rel d env,k+1) sign p)
-    | (_,(Some c),t as d)::sign, LetIn (na,_,_,p) ->
-      mkLetIn (na,c,t,aux (push_rel d env,k+1) sign p)
-    | _ -> assert false
-  in aux envk (List.rev sign) p
-
 (** Finding a subterm up to some testing function *)
 
 exception SubtermUnificationError of subterm_unification_error
@@ -95,7 +82,6 @@ exception NotUnifiable of (constr * constr * unification_error) option
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
-  get_evars : 'a -> Evd.evar_map;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
 }
@@ -105,7 +91,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo occs like_first test bywhat env cl occ t =
+let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -117,9 +103,9 @@ let replace_term_occ_gen_modulo occs like_first test bywhat env cl occ t =
     with NotUnifiable e when not like_first ->
       let lastpos = Option.get test.last_found in
      raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
-  let rec substrec (env,k) t =
+  let rec substrec k t =
     if nowhere_except_in && !pos > maxocc then t else
-    if not (Vars.closed0 t) then subst_below (env,k) t else
+    if not (Vars.closed0 t) then subst_below k t else
     try
       let subst = test.match_fun test.testing_state t in
       if Locusops.is_selected !pos occs then
@@ -132,51 +118,31 @@ let replace_term_occ_gen_modulo occs like_first test bywhat env cl occ t =
          add_subst t subst; incr pos;
          (* Check nested matching subterms *)
          if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then
-           begin nested := true; ignore (subst_below (env,k) t); nested := false end;
+           begin nested := true; ignore (subst_below k t); nested := false end;
          (* Do the effective substitution *)
          Vars.lift k (bywhat ()))
       else
-        (incr pos; subst_below (env,k) t)
+        (incr pos; subst_below k t)
     with NotUnifiable _ ->
-      subst_below (env,k) t
-  and subst_below (env,k) t =
-    match kind_of_term t with
-    | Case (ci,p,c,br) ->
-      let c = substrec (env,k) c in
-      let sigma = test.get_evars test.testing_state in
-      let t = Retyping.get_type_of env sigma c in
-      let IndType (indf,_) = find_rectype env sigma t in
-      let p = subst_cases_predicate (env,k) indf p in
-      let cstrs = get_constructors env indf in
-      let br = Array.map2 (subst_cases_branch (env,k) indf) br cstrs in
-      mkCase (ci,p,c,br)
-    | _ ->
-      map_constr_with_binders_left_to_right (fun d (env,k) -> (push_rel d env,k+1))
-        substrec (env,k) t
-  and subst_cases_predicate (env,k) indf p =
-    let arsign,_ = get_arity env indf in
-    let nrealargs = List.length arsign in
-    let (ind,params) = dest_ind_family indf in
-    let mind = applist (mkIndU ind,
-       (List.map (Vars.lift nrealargs) params)@(extended_rel_list 0 arsign)) in
-    process_under_binders substrec (env,k) ((Anonymous,None,mind)::arsign) p
-  and subst_cases_branch (env,k) indf b cstr =
-    process_under_binders substrec (env,k) cstr.cs_args b in
-  let t' = substrec (env,0) t in
+      subst_below k t
+  and subst_below k t =
+    map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+  in
+  let t' = substrec 0 t in
   (!pos, t')
 
-let replace_term_occ_modulo occs test bywhat env t =
+let replace_term_occ_modulo occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs' like_first test bywhat env None) occs' t
+    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
 
-let replace_term_occ_decl_modulo occs test bywhat env d =
+let replace_term_occ_decl_modulo occs test bywhat d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo plocs like_first test bywhat env)
+       (replace_term_occ_gen_modulo plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -190,30 +156,23 @@ let make_eq_univs_test env evd c =
 	with Evd.UniversesDiffer -> raise (NotUnifiable None)
       else raise (NotUnifiable None));
   merge_fun = (fun evd _ -> evd);
-  get_evars = (fun evd -> evd);
   testing_state = evd;
   last_found = None
 } 
 
-let subst_closed_term_occ env sigma occs c t =
-  let test = make_eq_univs_test env sigma c in
+let subst_closed_term_occ env evd occs c t =
+  let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
-  let typ = Retyping.get_type_of env sigma c in
-  assert (rel_context env == []);
-  let env = push_rel (Anonymous,Some c,typ) env in
-  let t' = replace_term_occ_modulo occs test bywhat env t in
+  let t' = replace_term_occ_modulo occs test bywhat t in
     t', test.testing_state
 
-let subst_closed_term_occ_decl env sigma occs c d =
-  let test = make_eq_univs_test env sigma c in
+let subst_closed_term_occ_decl env evd occs c d =
+  let test = make_eq_univs_test env evd c in
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   let bywhat () = mkRel 1 in
-  let typ = Retyping.get_type_of env sigma c in
-  assert (rel_context env == []);
-  let env = push_rel (Anonymous,Some c,typ) env in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat env None)
+       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 23d7ed9498..47d9654e57 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -29,7 +29,6 @@ exception SubtermUnificationError of subterm_unification_error
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
-  get_evars : 'a -> evar_map;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
 }
@@ -44,14 +43,14 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
 val replace_term_occ_modulo : occurrences or_like_first ->
-  'a testing_function -> (unit -> constr) -> env -> constr -> constr
+  'a testing_function -> (unit -> constr) -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
-  env -> named_declaration -> named_declaration
+  named_declaration -> named_declaration
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 002fd0c025..269c723e30 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1530,7 +1530,6 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | None, Some _ -> c2
     | None, None -> None in
   { match_fun = matching_fun; merge_fun = merge_fun;
-    get_evars = (function None -> sigma | Some (evd,_,_) -> evd);
     testing_state = None; last_found = None },
   (fun test -> match test.testing_state with
   | None -> None
@@ -1546,8 +1545,8 @@ let make_eq_test env evd c =
   (make_eq_univs_test env evd c, out)
 
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
-  let t = match ty with Some t -> t | None -> get_type_of env sigma c in
   let id =
+    let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
@@ -1555,8 +1554,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       errorlabstrm "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
-      x in
-  let env' = push_named (id, Some c, t) env in
+      x
+  in
   let likefirst = clause_with_generic_occurrences occs in
   let mkvarid () = mkVar id in
   let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
@@ -1572,7 +1571,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val d sign,depdecls)
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
-        let newdecl = replace_term_occ_decl_modulo occ test mkvarid env' d in
+        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
         then
@@ -1583,7 +1582,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
-        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid env' d in
+        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
@@ -1593,7 +1592,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo occ test mkvarid env' concl
+          replace_term_occ_modulo occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in