From 3e25c8d9f6e7802a2fc28697795b9128af731494 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Aug 2007 08:14:21 +0000
Subject: [PATCH] select now works correctly even if multiple hypotheses with
 the same name are present in the context.

---
 .../components/tactics/proofEngineHelpers.ml  | 26 +++++++++++++++----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index ec2e1919c..fa5c77d71 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -486,17 +486,33 @@ exception Fail of string Lazy.t
    let find_pattern_for name =
      try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
      with Not_found -> None in
+   (* Multiple hypotheses with the same name can be in the context.
+      In this case we need to pick the last one, but we will perform
+      a fold_right on the context. Thus we pre-process hyp_patterns. *)
+   let full_hyp_pattern =
+    let rec aux blacklist =
+     function
+        [] -> []
+      | None::tl -> None::aux blacklist tl
+      | Some (name,_)::tl ->
+         if List.mem name blacklist then
+          None::aux blacklist tl
+         else
+          find_pattern_for name::aux (name::blacklist) tl
+    in
+     aux [] context
+   in
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
-      (fun entry (subst,metasenv,ugraph,res,context) ->
+      (fun (pattern,entry) (subst,metasenv,ugraph,res,context) ->
         match entry with
-          None -> subst,metasenv,ugraph,(None::res),(None::context)
+          None -> subst,metasenv,ugraph,None::res,None::context
         | Some (name,Cic.Decl term) ->
-            (match find_pattern_for name with
+            (match pattern with
             | None ->
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
@@ -507,7 +523,7 @@ exception Fail of string Lazy.t
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
                   (entry::context))
         | Some (name,Cic.Def (bo, ty)) ->
-            (match find_pattern_for name with
+            (match pattern with
             | None ->
                let selected_ty=match ty with None -> None | Some _ -> Some [] in
                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
@@ -528,7 +544,7 @@ exception Fail of string Lazy.t
                 in
                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
                   (entry::context))
-      ) context (subst,metasenv,ugraph,[],[]))
+      ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[]))
     in
      subst,metasenv,ugraph,res
    in
-- 
2.39.2