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.ml  | 2 --
 proofs/proof_type.mli | 2 --
 proofs/tacexpr.ml     | 7 +++----
 3 files changed, 3 insertions(+), 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 5bd8060ae1..9f81ffee7f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -92,8 +92,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
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 0bd0eaa113..5fb463da73 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
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 2413e73ecf..6b153fa102 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -98,23 +98,22 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
-type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
      [Some l] means on hypothesis belonging to l *)
 type 'id gclause =
   { onhyps : 'id raw_hyp_location list option;
-    concl_occs : bool * int or_var list }
+    concl_occs : occurrences_expr }
 
 let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
 
-let simple_clause_of = function
+let goal_location_of = function
 | { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
       Some scl
 | { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
     None
 | _ ->
-    error "not a simple clause (one hypothesis or conclusion)"
+    error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
 
 type ('constr,'id) induction_clause = 
     ('constr with_bindings induction_arg list * 'constr with_bindings option * 
-- 
cgit v1.2.3