From 609a4bb85c88a5e5090f7db0a6bcf547ba9d0593 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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/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 -- 2.39.2