Bugs, nettoyage, et améliorations diverses

- vérification de la cohérence des ident pour éviter une option -R
  avec des noms non parsables (la vérification est faite dans
  id_of_string ce qui est très exigeant; faudrait-il une solution plus
  souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les 
  conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co

Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
  pattern -> et <-
- relecture de certaines parties du chapitre tactique


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

5 files changed, 68 insertions, 162 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index b2c279b39c..a477e3fd4b 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -73,7 +73,7 @@ let make_constr_action
 	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:constr_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "") in
+          let dummyid = Ident (dummy_loc,id_of_string "_") in
 	  make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
@@ -99,7 +99,7 @@ let make_cases_pattern_action
 	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "") in
+          let dummyid = Ident (dummy_loc,id_of_string "_") in
 	  make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
     | Some (p, (ETPattern | ETOther _)) :: tl -> 
 	failwith "Unexpected entry of type cases pattern or other" in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 522022bb32..28c2acb811 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -470,14 +470,22 @@ GEXTEND Gram
       | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
       (* Constructors *)
-      | IDENT "left"; bl = with_bindings -> TacLeft bl
-      | IDENT "right"; bl = with_bindings -> TacRight bl
-      | IDENT "split"; bl = with_bindings -> TacSplit (false,bl)
-      | "exists"; bl = bindings -> TacSplit (true,bl)
-      | "exists" -> TacSplit (true,NoBindings)
+      | IDENT "left";   bl = with_bindings -> TacLeft  (false,bl)
+      | IDENT "eleft";  bl = with_bindings -> TacLeft  (true,bl)
+      | IDENT "right";  bl = with_bindings -> TacRight (false,bl)
+      | IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
+      | IDENT "split";  bl = with_bindings -> TacSplit (false,false,bl)
+      | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl)
+      | "exists";       bl = bindings -> TacSplit (false,true,bl)
+      | "eexists";      bl = bindings -> TacSplit (true,true,bl)
+      | "exists"  (* meaningless? *)  -> TacSplit (false,true,NoBindings)
+      | "eexists"                     -> TacSplit (true,true,NoBindings)
       | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
-	  TacConstructor (n,l)
-      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
+	  TacConstructor (false,n,l)
+      | IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
+	  TacConstructor (true,n,l)
+      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t)
+      | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t)
 
       (* Equivalence relations *)
       | IDENT "reflexivity" -> TacReflexivity
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 800dc6a038..5d59a8489c 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -14,6 +14,7 @@
  * ast-based camlp4 *)
 
 open Pp
+open Util
 open Token
 
 (* Dictionaries: trees annotated with string options, each node being a map
@@ -76,8 +77,10 @@ let bad_token str = raise (Error (Bad_token str))
 
 (* Lexer conventions on tokens *)
 
-type utf8_token =
-    Utf8Letter of int | Utf8IdentPart of int | Utf8Symbol | AsciiChar
+type token_kind =
+  | Utf8Token of (utf8_status * int)
+  | AsciiChar
+  | EmptyStream
 
 let error_unsupported_unicode_character n cs =
   let bp = Stream.count cs in
@@ -121,123 +124,14 @@ let lookup_utf8_tail c cs =
 	  (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
       | _ -> error_utf8 cs
     in
-    match unicode land 0x1F000 with
-    | 0x0 ->
-    begin match unicode with
-    (* utf-8 Latin-1 non breaking space U00A0 *)
-    | 0x00A0 -> Utf8Letter n
-    (* utf-8 Latin-1 symbols U00A1-00BF *)
-    | x when 0x00A0 <= x & x <= 0x00BF -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00C0-00D6 *)
-    | x when 0x00C0 <= x & x <= 0x00D6 -> Utf8Letter n
-    (* utf-8 Latin-1 symbol U00D7 *)
-    | 0x00D7 -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00D8-00F6 *)
-    | x when 0x00D8 <= x & x <= 0x00F6 -> Utf8Letter n
-    (* utf-8 Latin-1 symbol U00F7 *)
-    | 0x00F7 -> Utf8Symbol
-    (* utf-8 Latin-1 letters U00F8-00FF *)
-    | x when 0x00F8 <= x & x <= 0x00FF -> Utf8Letter n
-    (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
-    | x when 0x0100 <= x & x <= 0x0241 -> Utf8Letter n
-    (* utf-8 Phonetic letters U0250-02AF *)
-    | x when 0x0250 <= x & x <= 0x02AF -> Utf8Letter n
-    (* utf-8 what do to with diacritics U0300-U036F ? *)
-    (* utf-8 Greek letters U0380-03FF *)
-    | x when 0x0380 <= x & x <= 0x03FF -> Utf8Letter n
-    (* utf-8 Cyrillic letters U0400-0481 *)
-    | x when 0x0400 <= x & x <= 0x0481 -> Utf8Letter n
-    (* utf-8 Cyrillic symbol U0482 *)
-    | 0x0482 -> Utf8Symbol
-    (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
-    (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
-    | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter n
-    (* utf-8 Cyrillic supplement letters U0500-U050F *)
-    | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter n
-    (* utf-8 Hebrew letters U05D0-05EA *)
-    | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter n
-    (* utf-8 Arabic letters U0621-064A *)
-    | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n
-    (* utf-8 Arabic supplement letters U0750-076D *)
-    | x when 0x0750 <= x & x <= 0x076D -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | 0x1000 ->
-    begin match unicode with
-    (* utf-8 Georgian U10A0-10FF (has holes) *)
-    | x when 0x10A0 <= x & x <= 0x10FF -> Utf8Letter n
-    (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
-    | x when 0x1100 <= x & x <= 0x11FF -> Utf8Letter n
-    (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
-    | x when 0x1E00 <= x & x <= 0x1E9B -> Utf8Letter n
-    | x when 0x1EA0 <= x & x <= 0x1EF9 -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | 0x2000 ->
-    begin match unicode with
-    (* utf-8 general punctuation U2080-2089 *)
-    (* Hyphens *)
-    | x when 0x2010 <= x & x <= 0x2011 -> Utf8Letter n 
-    (* Dashes and other symbols *)
-    | x when 0x2012 <= x & x <= 0x2027 -> Utf8Symbol
-    (* Per mille and per ten thousand signs *)
-    | x when 0x2030 <= x & x <= 0x2031 -> Utf8Symbol
-    (* Prime letters *)
-    | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> Utf8IdentPart n
-    (* Miscellaneous punctuation *)
-    | x when 0x2039 <= x & x <= 0x2056 -> Utf8Symbol
-    | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol
-    (* Invisible mathematical operators *)
-    | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol
-    (* utf-8 superscript U2070-207C *) 
-    | x when 0x2070 <= x & x <= 0x207C -> Utf8Symbol
-    (* utf-8 subscript U2080-2089 *) 
-    | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart n
-    (* utf-8 letter-like U2100-214F *)
-    | x when 0x2100 <= x & x <= 0x214F -> Utf8Letter n
-    (* utf-8 number-forms U2153-2183 *)
-    | x when 0x2153 <= x & x <= 0x2183 -> Utf8Symbol
-    (* utf-8 arrows A U2190-21FF *)
-    (* utf-8 mathematical operators U2200-22FF *)
-    (* utf-8 miscellaneous technical U2300-23FF *)
-    | x when 0x2190 <= x & x <= 0x23FF -> Utf8Symbol
-    (* utf-8 box drawing U2500-257F has ceiling, etc. *)
-    (* utf-8 block elements U2580-259F *)
-    (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
-    (* utf-8 miscellaneous symbols U2600-26FF *)
-    | x when 0x2500 <= x & x <= 0x26FF -> Utf8Symbol
-    (* utf-8 arrows B U2900-297F *)
-    | x when 0x2900 <= x & x <= 0x297F -> Utf8Symbol
-    (* utf-8 mathematical operators U2A00-2AFF *)
-    | x when 0x2A00 <= x & x <= 0x2AFF -> Utf8Symbol
-    (* utf-8 bold symbols U2768-U2775 *)
-    | x when 0x2768 <= x & x <= 0x2775 -> Utf8Symbol
-    (* utf-8 arrows and brackets U27E0-U27FF *)
-    | x when 0x27E0 <= x & x <= 0x27FF -> Utf8Symbol
-    (* utf-8 brackets, braces and parentheses *)
-    | x when 0x2980 <= x & x <= 0x299F -> Utf8Symbol
-    (* utf-8 miscellaneous including double-plus U29F0-U29FF *)
-    | x when 0x29F0 <= x & x <= 0x29FF -> Utf8Symbol
-    | _ -> error_unsupported_unicode_character n cs
-    end
-    | _ ->
-    begin match unicode with
-    (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
-    | x when 0x3040 <= x & x <= 0x30FF -> Utf8Letter n
-    (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
-    | x when 0x4E00 <= x & x <= 0x9FA5 -> Utf8Letter n
-    (* utf-8 Hangul syllables UAC00-D7AF *)
-    | x when 0xAC00 <= x & x <= 0xD7AF -> Utf8Letter n
-    (* utf-8 Gothic U10330-1034A *)
-    | x when 0x10330 <= x & x <= 0x1034A -> Utf8Letter n
-    | _ -> error_unsupported_unicode_character n cs
-    end
+    try classify_utf8 unicode, n
+    with UnsupportedUtf8 -> error_unsupported_unicode_character n cs
 	
 let lookup_utf8 cs =
   match Stream.peek cs with
-    | Some ('\x00'..'\x7F') -> Some AsciiChar
-    | Some ('\x80'..'\xFF' as c) -> Some (lookup_utf8_tail c cs)
-    | None -> None
+    | Some ('\x00'..'\x7F') -> AsciiChar
+    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs)
+    | None -> EmptyStream
 
 let check_special_token str =
   let rec loop_symb = parser
@@ -249,16 +143,16 @@ let check_special_token str =
 
 let check_ident str =
   let rec loop_id intail = parser
-    | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '_'); s >] ->
+    | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] ->
         loop_id true s
     | [< ' ('0'..'9' | ''') when intail; s >] ->
         loop_id true s
     | [< s >] ->
 	match lookup_utf8 s with
-	| Some (Utf8Letter n) -> njunk n s; loop_id true s
-	| Some (Utf8IdentPart n) when intail -> njunk n s; loop_id true s
-	| Some _ -> bad_token str
-	| None -> ()
+	| Utf8Token (Utf8Letter, n) -> njunk n s; loop_id true s
+	| Utf8Token (Utf8IdentPart, n) when intail -> njunk n s; loop_id true s
+	| EmptyStream -> ()
+	| Utf8Token _ | AsciiChar -> bad_token str
   in
   loop_id false (Stream.of_string str)
 
@@ -323,7 +217,7 @@ let rec ident_tail len = parser
       ident_tail (store len c) s
   | [< s >] ->
       match lookup_utf8 s with
-      | Some (Utf8IdentPart n | Utf8Letter n) ->
+      | Utf8Token ((Utf8IdentPart | Utf8Letter), n) ->
 	  ident_tail (nstore n len s) s
       | _ -> len
 
@@ -480,9 +374,9 @@ let parse_after_dot bp c =
       (constructor, get_buff len)
   | [< s >] ->
       match lookup_utf8 s with
-      | Some (Utf8Letter n) -> 
+      | Utf8Token (Utf8Letter, n) -> 
 	  (constructor, get_buff (ident_tail (nstore n 0 s) s))
-      | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None -> 
+      | AsciiChar | Utf8Token _ | EmptyStream -> 
 	  fst (process_chars bp c s)
 
 (* Parse a token in a char stream *)
@@ -518,16 +412,16 @@ let rec next_token = parser bp
       t
   | [< s >] ->
       match lookup_utf8 s with
-	| Some (Utf8Letter n) ->
+	| Utf8Token (Utf8Letter, n) ->
 	    let len = ident_tail (nstore n 0 s) s in
 	    let id = get_buff len in
 	    let ep = Stream.count s in
 	    comment_stop bp;
 	    (try ("",find_keyword id) with Not_found -> ("IDENT",id)), (bp, ep)
-	| Some (Utf8Symbol | AsciiChar | Utf8IdentPart _) -> 
+	| AsciiChar | Utf8Token ((Utf8Symbol | Utf8IdentPart), _) -> 
 	    let t = process_chars bp (Stream.next s) s in
 	    comment_stop bp; t
-	| None ->
+	| EmptyStream ->
 	    comment_stop bp; (("EOI", ""), (bp, bp + 1))
 
 (* Location table system for creating tables associating a token count
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d4a809756c..55c6a4387e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -133,6 +133,8 @@ let rec pr_message_token prid = function
 
 let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
+let with_evars ev s = if ev then "e" ^ s else s
+
 let out_bindings = function
   | ImplicitBindings l -> ImplicitBindings (List.map snd l)
   | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
@@ -637,7 +639,8 @@ let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
   | TacIntroMove (None,None) -> str "intro"
   | TacAssumption -> str "assumption"
-  | TacAnyConstructor None -> str "constructor"
+  | TacAnyConstructor (false,None) -> str "constructor"
+  | TacAnyConstructor (true,None) -> str "econstructor"
   | TacTrivial ([],Some []) -> str "trivial"
   | TacAuto (None,[],Some []) -> str "auto"
   | TacReflexivity -> str "reflexivity"
@@ -674,14 +677,14 @@ and pr_atom1 = function
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
   | TacApply (a,ev,cb) ->
       hov 1 ((if a then mt() else str "simple ") ++
-             str (if ev then "eapply" else "apply") ++ spc () ++ 
+             str (with_evars ev "apply") ++ spc () ++ 
              pr_with_bindings cb)
   | TacElim (ev,cb,cbo) ->
-      hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ 
+      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
   | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
   | TacCase (ev,cb) ->
-      hov 1 (str (if ev then "ecase" else "case") ++ spc () ++ pr_with_bindings cb)
+      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
@@ -724,14 +727,14 @@ and pr_atom1 = function
   | TacSimpleInduction h ->
       hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewInduction (ev,h,e,ids) ->
-      hov 1 (str (if ev then "einduction" else "induction") ++ spc () ++
+      hov 1 (str (with_evars ev "induction") ++ spc () ++
 	     prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (ev,h,e,ids) ->
-      hov 1 (str (if ev then "edestruct" else "destruct") ++ spc () ++
+      hov 1 (str (with_evars ev "destruct") ++ spc () ++
              prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ 
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
@@ -792,15 +795,16 @@ and pr_atom1 = function
       hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) 
 
   (* Constructors *)
-  | TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
-  | TacRight l -> hov 1 (str "right" ++ pr_bindings l)
-  | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings l)
-  | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings l)
-  | TacAnyConstructor (Some t) ->
-      hov 1 (str "constructor" ++ pr_arg (pr_tac_level (latom,E)) t)
-  | TacAnyConstructor None as t -> pr_atom0 t
-  | TacConstructor (n,l) ->
-      hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
+  | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
+  | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
+  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ pr_bindings l)
+  | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ pr_ex_bindings l)
+  | TacAnyConstructor (ev,Some t) ->
+      hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
+  | TacAnyConstructor (ev,None) as t -> pr_atom0 t
+  | TacConstructor (ev,n,l) ->
+      hov 1 (str (with_evars ev "constructor") ++ 
+             pr_or_metaid pr_intarg n ++ pr_bindings l)
 
   (* Conversion *)  
   | TacReduce (r,h) ->
@@ -825,7 +829,7 @@ and pr_atom1 = function
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
-      hov 1 (str (if ev then "erewrite" else "rewrite") ++ 
+      hov 1 (str (with_evars ev "rewrite") ++ 
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) -> 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d961dc2f2e..e698a187c9 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -372,18 +372,18 @@ let rec mlexpr_of_atomic_tactic = function
               $mlexpr_of_hyp id2$ >>
 
   (* Constructors *)
-  | Tacexpr.TacLeft l ->
-      <:expr< Tacexpr.TacLeft $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacRight l ->
-      <:expr< Tacexpr.TacRight $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacSplit (b,l) ->
+  | Tacexpr.TacLeft (ev,l) ->
+      <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
+  | Tacexpr.TacRight (ev,l) ->
+      <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
+  | Tacexpr.TacSplit (ev,b,l) ->
       <:expr< Tacexpr.TacSplit
-        ($mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
-  | Tacexpr.TacAnyConstructor t ->
-      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_option mlexpr_of_tactic t$>>
-  | Tacexpr.TacConstructor (n,l) ->
+        ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
+  | Tacexpr.TacAnyConstructor (ev,t) ->
+      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
+  | Tacexpr.TacConstructor (ev,n,l) ->
       let n = mlexpr_of_or_metaid mlexpr_of_int n in
-      <:expr< Tacexpr.TacConstructor $n$ $mlexpr_of_binding_kind l$>>
+      <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
 
   (* Conversion *)
   | Tacexpr.TacReduce (r,cl) ->