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

1 files changed, 3 insertions, 4 deletions

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 2413e73ec..6b153fa10 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 *