aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-05-18 17:14:23 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-05-18 17:14:23 +0000
commitc32efcb1b44108f321a1cd2e7d42cd8cabe3170c (patch)
tree070f9117d7192e5f73d692cf173e773930af1926
parent53fc67702b49df15af5695411e3c97941e8fd837 (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.ml16
-rw-r--r--test-suite/success/refine.v18
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.