diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-16 08:18:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-16 08:18:53 +0000 |
| commit | 171c73b40b985f604e4d6c1529fb28d1dfa8e300 (patch) | |
| tree | ca36754a96d68fcedf329fb5217d41c171c30008 /tactics/dhyp.ml | |
| parent | 208f162ab68d00488248ee052947592dd23d5d52 (diff) | |
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index b7929b29a..35d2e1324 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -296,11 +296,11 @@ let set_extern_interp f = forward_interp_tactic := f let applyDestructor cls discard dd gls = match_dpat dd.d_pat cls gls; - let cll = simple_clause_list_of cls gls in + let cll = simple_clause_of cls gls in let tacl = List.map (fun cl -> match cl, dd.d_code with - | Some ((_,id),_), (Some x, tac) -> + | Some id, (Some x, tac) -> let arg = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in TacLetIn (false, [(dummy_loc, x), arg], tac) @@ -311,7 +311,7 @@ let applyDestructor cls discard dd gls = let discard_0 = List.map (fun cl -> match (cl,dd.d_pat) with - | (Some ((_,id),_),HypLocation(discardable,_,_)) -> + | (Some id,HypLocation(discardable,_,_)) -> if discard & discardable then thin [id] else tclIDTAC | (None,ConclLocation _) -> tclIDTAC | _ -> error "ApplyDestructor" ) cll in @@ -357,9 +357,9 @@ let rec search n = [intros; assumption; (tclTHEN - (Tacticals.tryAllClauses + (Tacticals.tryAllHypsAndConcl (function - | Some ((_,id),_) -> (dHyp id) + | Some id -> (dHyp id) | None -> dConcl )) (search (n-1)))] |