From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Apr 2007 15:08:33 +0000 (+0000)
Subject: fixed case
X-Git-Tag: 0.4.95@7852~536
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=609a4bb85c88a5e5090f7db0a6bcf547ba9d0593;p=helm.git

fixed case
---

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 8787b1a73..50626aff0 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/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