- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to

  change the default pretty-printing to use Π, λ instead of
  forall and fun (and allow "," as well as "=>" for "fun" to be more
  consistent with the standard forall and exists syntax). Parsing allows
  theses new forms too, even if not in -unicode, and does not make Π or
  λ keywords. As usual, criticism and suggestions are welcome :)
  Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
  for tactics. 
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
  combination.
- Backtrack on [Enriching] modifier, now used exclusively in the 
  implementation of implicit arguments.


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

16 files changed, 103 insertions, 71 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9db1c7dc4..1095228b5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2111,7 +2111,7 @@ let rec xlate_vernac =
   | VernacNop -> CT_proof_no_op
   | VernacComments l -> 
       CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
-  | VernacDeclareImplicits(true, id, _, opt_positions) ->
+  | VernacDeclareImplicits(true, id, opt_positions) ->
       CT_implicits
 	(reference_to_ct_ID id,
 	 match opt_positions with
@@ -2124,7 +2124,7 @@ let rec xlate_vernac =
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
 		     | ExplByName id, _, _ -> CT_ident (string_of_id id)) l)))
-  | VernacDeclareImplicits(false, id, _, opt_positions) ->
+  | VernacDeclareImplicits(false, id, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
       CT_reserve(CT_id_ne_list(xlate_ident a, 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index fc5f4e4cb..7ef9078db 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -832,7 +832,7 @@ possible with the syntax:
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
 \end{quote}
-
+\medskip
 It is also possible to \emph{redefine} an existing user-defined tactic
 using the syntax:
 \begin{quote}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5ccbaf130..44c519e99 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2008,16 +2008,18 @@ must have the form
 \noindent where \texttt{eq} is the Leibniz equality or a registered
 setoid equality.
 
-\noindent Then {\tt rewrite \term} replaces every occurrence of 
-\term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are
+\noindent Then {\tt rewrite \term} finds the first subterm matching
+\term$_1$ in the goal, resulting in instances \term$_1'$ and \term$_2'$
+and then replaces every occurrence of \term$_1'$ by \term$_2'$.
+Hence, some of the variables x$_i$ are
 solved by unification, and some of the types \texttt{A}$_1$, \dots,
 \texttt{A}$_n$ become new subgoals.
 
-\Rem In case the type of  
-\term$_1$ contains occurrences of variables bound in the
-type of \term, the tactic tries first to find a subterm of the goal
-which matches this term in order to find a closed instance \term$'_1$
-of \term$_1$, and then all instances of \term$'_1$ will be replaced.
+% \Rem In case the type of  
+% \term$_1$ contains occurrences of variables bound in the
+% type of \term, the tactic tries first to find a subterm of the goal
+% which matches this term in order to find a closed instance \term$'_1$
+% of \term$_1$, and then all instances of \term$'_1$ will be replaced.
 
 \begin{ErrMsgs}
 \item \errindex{The term provided does not end with an equation}
@@ -2056,6 +2058,21 @@ This happens if \term$_1$ does not occur in the goal.
   Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
   inserted before the term to rewrite.
 
+\item {\tt rewrite {\term} at \textit{occurrences}}
+  \tacindex{rewrite \dots\ at}
+
+  Rewrite only the given occurrences of \term$_1'$. Occurrences are
+  specified from left to right as for \texttt{pattern} (\S
+  \ref{pattern}). The rewrite is always performed using setoid
+  rewriting, even for leibniz equality, so one has to 
+  \texttt{Import Setoid} to use this variant.
+
+\item {\tt rewrite {\term} by {\tac}}
+  \tacindex{rewrite \dots\ by}
+
+  Use {\tac} to completely solve the side-conditions arising from the
+  rewrite.
+
 \item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
   Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
   up to {\tt rewrite $\term_n$}, each one working on the first subgoal
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 8bdf6ab0a..d2b6d1151 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -540,7 +540,7 @@ the prefixed tactics it is possible to pass additional arguments such as
 
 The \texttt{using relation}
 arguments cannot be passed to the unprefixed form. The latter argument
-tells the  tactic what parametric  relation should be used  to replace
+tells the tactic what parametric relation should be used to replace
 the first tactic argument with the second one. If omitted, it defaults
 to the \texttt{DefaultRelation} instance on the type of the objects.
 By default, it means the most recent \texttt{Equivalence} instance in
@@ -679,7 +679,7 @@ If a signature mentions a relation $R$ on the left of an arrow
 is smaller than $R$, and the inverse applies on the right of an arrow. 
 One can then declare only a few morphisms instances that generate the complete set
 of signatures for a particular constant. By default, the only declared
-subrelations is \texttt{iff}, which is a subrelation of \texttt{impl}
+subrelation is \texttt{iff}, which is a subrelation of \texttt{impl}
 and \texttt{inverse impl} (the dual of implication). That's why we can
 declare only two morphisms for conjunction:
 \verb|Morphism (impl ==> impl ==> impl) and| and 
diff --git a/lib/flags.ml b/lib/flags.ml
index 60d6c7836..36179bc8a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -32,6 +32,8 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
+let unicode_syntax = ref false
+
 (* Translate *)
 let translate = ref false
 let make_translate f = translate := f
diff --git a/lib/flags.mli b/lib/flags.mli
index c14e223e7..2301d8a0d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -27,6 +27,8 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
+val unicode_syntax : bool ref
+
 val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 25a7d0b69..b4bac06e8 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -205,10 +205,20 @@ GEXTEND Gram
                 CNotation(loc,"( _ )",[c])
             | _ -> c) ] ]
   ;
+  forall: 
+    [ [ "forall" -> () 
+    | IDENT "Π" -> ()
+    ] ]
+  ;
+  lambda: 
+    [ [ "fun" -> () 
+    | IDENT "λ" -> ()
+    ] ]
+  ;
   binder_constr:
-    [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+    [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c
-      | "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" ->
+      | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
           mkCLambdaN loc bl c
       | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d59a46d12..5cd173292 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -205,7 +205,8 @@ GEXTEND Gram
       | s = ne_string -> ByNotation (loc,s) ] ]
   ;
   occs:
-    [ [ "at"; nl = LIST1 int_or_var -> nl
+    [ [ "at"; nl = LIST1 integer -> List.map (fun x -> Rawterm.ArgArg x) nl
+      | "at"; id = identref -> [Rawterm.ArgVar id]
       | -> [] ] ]
   ;
   pattern_occ:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4eafbd68c..2efe88c0c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -495,49 +495,39 @@ GEXTEND Gram
 	  VernacContext c
 	    
       | global = [ IDENT "Global" -> true | -> false ];
-	 IDENT "Instance"; name = OPT identref; sup = OPT [ l = binders_let -> l ];
-(* 	 name' = OPT [ "=>"; id = identref -> id ]; *)
-	 ":" ; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
+	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
-	   let sup = match sup with None -> [] | Some l -> l in
-	   let is = (* We reverse the default binding mode on the right *)
-	     let n = 
-	       match name with
-		 | Some (loc, id) -> (loc, Name id)
-		 | None -> (dummy_loc, Anonymous)
-	     in
-	       n, expl, t 
+	   let sup =
+	     match sup with
+		 None -> []
+	       | Some l -> l
 	   in
-	     VernacInstance (global, sup, is, props, pri)
+	   let n = 
+	     let (loc, id) = name in 
+	       (loc, Name id)
+	   in
+	     VernacInstance (global, sup, (n, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ];
+      | IDENT "Implicit"; IDENT "Arguments"; 
 	   local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; 
 	   qid = global; 
 	   pos = OPT [ "["; l = LIST0 implicit_name; "]" -> 
-		   List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   VernacDeclareImplicits (local,qid,enrich,pos)
+	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
+	   VernacDeclareImplicits (local,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
-
-(*   typeclass_ctx:  *)
-(*     [ [ sup = LIST1 operconstr SEP "->"; "=>" -> sup *)
-(*     ] ] *)
-(*   ; *)
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
     | id = ident -> (id,false,false)
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-(*   typeclass_param_type: *)
-(*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
-(*     | id = identref -> id, CHole (loc, None) ] ] *)
-(*   ; *)
   typeclass_field_type:
     [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ]
   ;
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 41d98f2bc..44aabc2cb 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -218,13 +218,13 @@ let begin_of_binders = function
 let surround_binder k p = 
   match k with
       Default Explicit -> hov 1 (str"(" ++ p ++ str")")
-    | Default Implicit -> hov 1 (str"`" ++ p ++ str"`")
+    | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
     | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
 
 let surround_implicit k p =
   match k with
       Default Explicit -> p
-    | Default Implicit -> (str"`" ++ p ++ str"`")
+    | Default Implicit -> (str"{" ++ p ++ str"}")
     | TypeClass b -> (str"[" ++ p ++ str"]")
 
 let pr_binder many pr (nal,k,t) =
@@ -472,6 +472,16 @@ let pr_app pr a l =
     pr (lapp,L) a  ++ 
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
+let pr_forall () =
+  if !Flags.unicode_syntax then str"Π" ++ spc ()
+  else str"forall" ++ spc ()
+
+let pr_fun () =
+  if !Flags.unicode_syntax then str"λ" ++ spc ()
+  else str"fun" ++ spc ()
+
+let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>")
+
 let rec pr sep inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
@@ -492,17 +502,16 @@ let rec pr sep inherited a =
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
       hov 0 (
-	hov 2 (pr_delimited_binders (fun () -> str"forall" ++ spc())
+	hov 2 (pr_delimited_binders pr_forall
                  (pr mt ltop) bl) ++
         str "," ++ pr spc ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
       hov 0 (
-        hov 2 (pr_delimited_binders (fun () -> str"fun" ++ spc())
-                 (pr mt ltop) bl) ++
-
-        str " =>" ++ pr spc ltop a),
+        hov 2 (pr_delimited_binders pr_fun
+                (pr mt ltop) bl) ++
+	  Lazy.force pr_fun_sep ++ pr spc ltop a),
       llambda
   | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
@@ -569,8 +578,8 @@ let rec pr sep inherited a =
         pr spc ltop b),
       lletin
   | CIf (_,c,(na,po),b1,b2) ->
-      (* On force les parenthèses autour d'un "if" sous-terme (même si le
-	 parsing est lui plus tolérant) *)
+      (* On force les parenthèses autour d'un "if" sous-terme (même si le
+	 parsing est lui plus tolérant) *)
       hv 0 (
 	hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++
 	spc () ++
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bd87e09c6..a863665a9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -818,12 +818,12 @@ let rec pr_vernac = function
         (str"Notation " ++ pr_locality local ++ pr_id id ++ 
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (local,q,e,None) ->
+  | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (local,q,e,Some imps) ->
+  | VernacDeclareImplicits (local,q,Some imps) ->
       hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++
-      spc() ++ pr_reference q ++ spc() ++
-             str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	spc() ++ pr_reference q ++ spc() ++
+	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index aeaa197e8..aea6f5d7a 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -76,23 +76,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   setoidreplaceinat (default_relation x y) id idtac o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplace (default_relation x y) ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "at" int_or_var_list(o) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceat (default_relation x y) ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "in" hyp(id) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplacein (default_relation x y) id ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "in" hyp(id) 
   "at" int_or_var_list(o) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceinat (default_relation x y) id ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
@@ -106,13 +106,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplace (rel x y) ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
   "at" int_or_var_list(o)  
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceat (rel x y) ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
@@ -129,14 +129,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel)
   "in" hyp(id)
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplacein (rel x y) id ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
   "in" hyp(id)
   "at" int_or_var_list(o)  
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceinat (rel x y) id ltac:t o.
 
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d24312ff1..cbc3b02ad 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -4,7 +4,7 @@ Require Import ProofIrrelevance.
 
 Open Local Scope program_scope.
 
-Implicit Arguments Enriching Acc_inv [y].
+Implicit Arguments Acc_inv [A R x y].
 
 (** Reformulation of the Wellfounded module using subsets where possible. *)
 
@@ -137,11 +137,10 @@ Section Well_founded_measure.
       apply Fix_measure_F_inv.
     Qed.
 
-    Lemma fix_measure_sub_eq :
-        forall x : A,
-          Fix_measure_sub P F_sub x =
-          let f_sub := F_sub in
-            f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
+    Lemma fix_measure_sub_eq : forall x : A,
+      Fix_measure_sub P F_sub x =
+        let f_sub := F_sub in
+          f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
       exact Fix_measure_eq.
     Qed.
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a4dee4b6e..d09a87dc6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -253,7 +253,9 @@ let parse_args is_ide =
     | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
     | "-emacs-U" :: rem -> Flags.print_emacs := true; 
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-	  
+	
+    | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+
     | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
     | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e9b49e7e8..c705d0287 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -681,9 +681,9 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits local r e = function
+let vernac_declare_implicits local r = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (global_with_alias r) e
+      Impargs.declare_manual_implicits local (global_with_alias r) false
 	(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
   | None -> 
       Impargs.declare_implicits local (global_with_alias r)
@@ -1266,7 +1266,7 @@ let interp c = match c with
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (local,qid,e,l) ->vernac_declare_implicits local qid e l
+  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 16589805f..986c63c0b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -290,7 +290,7 @@ type vernac_expr =
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
-  | VernacDeclareImplicits of locality_flag * lreference * bool *
+  | VernacDeclareImplicits of locality_flag * lreference * 
       (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list