diff options
| author | herbelin | 2009-03-16 08:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2009-03-16 08:18:53 +0000 |
| commit | 171c73b40b985f604e4d6c1529fb28d1dfa8e300 (patch) | |
| tree | ca36754a96d68fcedf329fb5217d41c171c30008 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 447bb734a7..801c0334b4 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -418,13 +418,13 @@ let pr_hyp_location pr_id = function let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) -let pr_simple_clause pr_id = function +let pr_simple_hyp_clause pr_id = function | [] -> mt () | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) let pr_in_hyp_as pr_id = function | None -> mt () - | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat + | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat let pr_clauses pr_id = function | { onhyps=None; concl_occs=occs } -> @@ -869,11 +869,11 @@ and pr_atom1 = function | TacInversion (NonDepInversion (k,cl,ids),hyp) -> hov 1 (pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ - pr_with_inversion_names ids ++ pr_simple_clause pr_ident cl) + pr_with_inversion_names ids ++ pr_simple_hyp_clause pr_ident cl) | TacInversion (InversionUsing (c,cl),hyp) -> hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ spc () ++ str "using" ++ spc () ++ pr_constr c ++ - pr_simple_clause pr_ident cl) + pr_simple_hyp_clause pr_ident cl) in |