diff options
author | 2007-05-18 17:14:23 +0000 | |
---|---|---|
committer | 2007-05-18 17:14:23 +0000 | |
commit | c32efcb1b44108f321a1cd2e7d42cd8cabe3170c (patch) | |
tree | 070f9117d7192e5f73d692cf173e773930af1926 | |
parent | 53fc67702b49df15af5695411e3c97941e8fd837 (diff) |
Wish #1582 (3eme)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/refine.ml | 16 | ||||
-rw-r--r-- | test-suite/success/refine.v | 18 |
2 files changed, 28 insertions, 6 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index bfab02064..a9fdfacb8 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -327,12 +327,16 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | LetIn (Name id,c1,t1,c2), _ -> tclTHENS (assert_tac true (Name id) t1) - [(match sgp with - | [None] -> tclIDTAC - | [Some th] -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th) - | _ -> assert false); - exact_check (subst1 (mkVar id) c2)] - gl + [(match List.hd sgp with + | None -> tclIDTAC + | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)); + (match List.tl sgp with + | [] -> refine (subst1 (mkVar id) c2) (* a complete proof *) + | [None] -> tclIDTAC (* a meta *) + | [Some th] -> (* a partial proof *) + onLastHyp (fun id -> tcc_aux (mkVar id::subst) th) + | _ -> assert false)] + gl (* fix => tactique Fix *) | Fix ((ni,_),(fi,ai,_)) , _ -> diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 793cddb82..4b636618a 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -99,3 +99,21 @@ Goal intros. refine (@proj1 _ _ (H 0 _ _)). Abort. + +(* Use to fail because let-in with metas in the body where rejected + because a priori considered as dependent *) + +Require Import Peano_dec. + +Definition fact_F : + forall (n:nat), + (forall m, m<n -> nat) -> + nat. +refine + (fun n fact_rec => + if eq_nat_dec n 0 then + 1 + else + let fn := fact_rec (n-1) _ in + n * fn). +Abort. |