From 41f42a44652a652346e5725f646ddeb621e27c89 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Apr 2007 15:08:33 +0000
Subject: [PATCH] fixed case

---
 .../components/tactics/primitiveTactics.ml    | 31 +++++++++++++------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 8787b1a73..50626aff0 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -700,22 +700,35 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
     let n_right_args = List.length right_args in
     let n_lambdas = n_right_args + 1 in
     let lifted_ty = CicSubstitution.lift n_lambdas ty in
-    let replace = ProofEngineReduction.replace_lifting
-       ~equality:(CicUtil.alpha_equivalence)
-    in
     let captured_ty = 
       let what = 
-        List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
+        List.map (CicSubstitution.lift n_lambdas) (right_args)
       in
-      let with_what = 
+      let with_what meta = 
         let rec mkargs = function 
-          | 0 -> []
-          | 1 -> [Cic.Rel 1]
-          | n -> (Cic.Rel n)::(mkargs (n-1)) 
+          | 0 -> assert false
+          | 1 -> []
+          | n -> 
+              (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1)) 
         in
         mkargs n_lambdas 
       in
-      replace ~what ~with_what ~where:lifted_ty
+      let replaced = ref false in
+      let replace = ProofEngineReduction.replace_lifting
+       ~equality:(fun a b -> let rc = CicUtil.alpha_equivalence a b in 
+                  if rc then replaced := true; rc)
+      in
+      let captured = 
+        replace ~what:[CicSubstitution.lift n_lambdas term] 
+          ~with_what:[Cic.Rel 1] ~where:lifted_ty
+      in
+      if not !replaced then
+        (* this means the matched term is not there, 
+         * but maybe right params are: we user rels (to right args lambdas) *)
+        replace ~what ~with_what:(with_what false) ~where:captured
+      else
+        (* since the matched is there, rights should be inferrable *)
+        replace ~what ~with_what:(with_what true) ~where:captured
     in
     let captured_term_ty = 
       let term_ty = CicSubstitution.lift n_right_args termty in
-- 
2.39.2