diff options
| -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 bfab02064e..a9fdfacb89 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 793cddb826..4b636618ad 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. |