- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index bc483cfc3..f80deab10 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -131,18 +131,24 @@ val subst_term : constr -> constr -> constr
 (* [replace_term d e c] replaces [d] by [e] in [c] *)
 val replace_term : constr -> constr -> constr -> constr
 
+(* In occurrences sets, false = everywhere except and true = nowhere except *)
+type occurrences = bool * int list
+val all_occurrences : occurrences
+val no_occurrences_in_set : occurrences
+
 (* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at
    positions [occl], counting from [n], by [Rel 1] in [d] *)
-val subst_term_occ_gen : int list -> int -> constr -> types -> int * types
+val subst_term_occ_gen : 
+  occurrences -> int -> constr -> types -> int * types
 
 (* [subst_term_occ occl c d] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
-val subst_term_occ : int list -> constr -> constr -> constr
+val subst_term_occ : occurrences -> constr -> constr -> constr
 
 (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [decl] *)
 val subst_term_occ_decl :
-  int list -> constr -> named_declaration -> named_declaration
+  occurrences -> constr -> named_declaration -> named_declaration
 
 val error_invalid_occurrence : int list -> 'a