diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-18 17:14:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-18 17:14:23 +0000 |
| commit | c32efcb1b44108f321a1cd2e7d42cd8cabe3170c (patch) | |
| tree | 070f9117d7192e5f73d692cf173e773930af1926 /tactics | |
| parent | 53fc67702b49df15af5695411e3c97941e8fd837 (diff) | |
Wish #1582 (3eme)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 16 |
1 files changed, 10 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,_)) , _ -> |