From 171c73b40b985f604e4d6c1529fb28d1dfa8e300 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 16 Mar 2009 08:18:53 +0000 Subject: 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 --- proofs/proof_type.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'proofs/proof_type.mli') diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 0bd0eaa11..5fb463da7 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -127,8 +127,6 @@ and tactic_arg = glob_tactic_expr) Tacexpr.gen_tactic_arg -type hyp_location = identifier Tacexpr.raw_hyp_location - type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant -- cgit v1.2.3