simplify has a brand new semantics!

[helm.git] / components / tactics / primitiveTactics.ml

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 8787b1a73c048e6b523ccf75dc85906509d64746..cc16c203012101be0aff7f3657da38dded372b8d 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -700,22 +700,36 @@ 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)
+       ~context:[]
+      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