Proper handling of exception definition in Ltac2.

We actually implemented a full-fledged open type system, so that
exceptions are a special case of it.

13 files changed, 398 insertions, 58 deletions

diff --git a/Init.v b/Init.v
index 0f0b4636d8..322f275346 100644
--- a/Init.v
+++ b/Init.v
@@ -20,7 +20,7 @@ Ltac2 Type evar.
 Ltac2 Type constr.
 Ltac2 Type ident.
 Ltac2 Type message.
-Ltac2 Type exn.
+Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
 
 (** Pervasive types *)
diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index 9384584f19..a149d942c6 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -137,6 +137,7 @@ GEXTEND Gram
   ;
   tac2typ_knd:
     [ [ t = tac2type -> CTydDef (Some t)
+      | "["; ".."; "]" -> CTydOpn
       | "["; t = tac2alg_constructors; "]" -> CTydAlg t
       | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ]
   ;
@@ -173,9 +174,12 @@ GEXTEND Gram
     ] ]
   ;
   tac2typ_def:
-    [ [ prm = tac2typ_prm; id = locident; ":="; e = tac2typ_knd ->
-        (id, (prm, e))
-      | prm = tac2typ_prm; id = locident -> (id, (prm, CTydDef None))
+    [ [ prm = tac2typ_prm; id = Prim.qualid; (r, e) = tac2type_body -> (id, r, (prm, e)) ] ]
+  ;
+  tac2type_body:
+    [ [ -> false, CTydDef None
+      | ":="; e = tac2typ_knd -> false, e
+      | "::="; e = tac2typ_knd -> true, e
     ] ]
   ;
   tac2def_typ:
diff --git a/tac2core.ml b/tac2core.ml
index c18b6032a6..227bea8ddd 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -109,8 +109,14 @@ let to_constr c = to_ext val_constr c
 let of_ident c = of_ext val_ident c
 let to_ident c = to_ext val_ident c
 
-let of_exn c = of_ext val_exn c
-let to_exn c = to_ext val_exn c
+(** FIXME: handle backtrace in Ltac2 exceptions *)
+let of_exn c = match fst c with
+| LtacError (kn, c) -> ValOpn (kn, c)
+| _ -> of_ext val_exn c
+
+let to_exn c = match c with
+| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
+| _ -> to_ext val_exn c
 
 let of_pp c = of_ext val_pp c
 let to_pp c = to_ext val_pp c
diff --git a/tac2entries.ml b/tac2entries.ml
index f4b3147c48..c776ad13d4 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -19,6 +19,8 @@ open Tac2print
 open Tac2intern
 open Vernacexpr
 
+(** Tactic definition *)
+
 type tacdef = {
   tacdef_local : bool;
   tacdef_expr : glb_tacexpr;
@@ -52,6 +54,8 @@ let inTacDef : tacdef -> obj =
      subst_function = subst_tacdef;
      classify_function = classify_tacdef}
 
+(** Type definition *)
+
 type typdef = {
   typdef_local : bool;
   typdef_expr : glb_quant_typedef;
@@ -86,6 +90,8 @@ let push_typedef visibility sp kn (_, def) = match def with
   in
   Tac2env.push_type visibility sp kn;
   List.iter iter fields
+| GTydOpn ->
+  Tac2env.push_type visibility sp kn
 
 let next i =
   let ans = !i in
@@ -108,7 +114,7 @@ let define_typedef kn (params, def as qdef) = match def with
       Tac2env.cdata_prms = params;
       cdata_type = kn;
       cdata_args = args;
-      cdata_indx = tag;
+      cdata_indx = Some tag;
     } in
     Tac2env.define_constructor knc data
   in
@@ -129,6 +135,8 @@ let define_typedef kn (params, def as qdef) = match def with
   in
   Tac2env.define_type kn qdef;
   List.iteri iter fs
+| GTydOpn ->
+  Tac2env.define_type kn qdef
 
 let perform_typdef vs ((sp, kn), def) =
   let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in
@@ -155,6 +163,78 @@ let inTypDef : typdef -> obj =
      subst_function = subst_typdef;
      classify_function = classify_typdef}
 
+(** Type extension *)
+
+type extension_data = {
+  edata_name : Id.t;
+  edata_args : int glb_typexpr list;
+}
+
+type typext = {
+  typext_local : bool;
+  typext_prms : int;
+  typext_type : type_constant;
+  typext_expr : extension_data list;
+}
+
+let push_typext vis sp kn def =
+  let iter data =
+    let spc = change_sp_label sp data.edata_name in
+    let knc = change_kn_label kn data.edata_name in
+    Tac2env.push_ltac vis spc (TacConstructor knc)
+  in
+  List.iter iter def.typext_expr
+
+let define_typext kn def =
+  let iter data =
+    let knc = change_kn_label kn data.edata_name in
+    let cdata = {
+      Tac2env.cdata_prms = def.typext_prms;
+      cdata_type = def.typext_type;
+      cdata_args = data.edata_args;
+      cdata_indx = None;
+    } in
+    Tac2env.define_constructor knc cdata
+  in
+  List.iter iter def.typext_expr
+
+let cache_typext ((sp, kn), def) =
+  let () = define_typext kn def in
+  push_typext (Until 1) sp kn def
+
+let perform_typext vs ((sp, kn), def) =
+  let () = if not def.typext_local then push_typext vs sp kn def in
+  define_typext kn def
+
+let load_typext i obj = perform_typext (Until i) obj
+let open_typext i obj = perform_typext (Exactly i) obj
+
+let subst_typext (subst, e) =
+  let open Mod_subst in
+  let subst_data data =
+    let edata_args = List.smartmap (fun e -> subst_type subst e) data.edata_args in
+    if edata_args == data.edata_args then data
+    else { data with edata_args }
+  in
+  let typext_type = subst_kn subst e.typext_type in
+  let typext_expr = List.smartmap subst_data e.typext_expr in
+  if typext_type == e.typext_type && typext_expr == e.typext_expr then
+    e
+  else
+    { e with typext_type; typext_expr }
+
+let classify_typext o = Substitute o
+
+let inTypExt : typext -> obj =
+  declare_object {(default_object "TAC2-TYPE-EXTENSION") with
+     cache_function  = cache_typext;
+     load_function   = load_typext;
+     open_function   = open_typext;
+     subst_function = subst_typext;
+     classify_function = classify_typext}
+
+(** Toplevel entries *)
+
 let register_ltac ?(local = false) isrec tactics =
   if isrec then
     let map (na, e) = (na, None, e) in
@@ -206,7 +286,12 @@ let register_ltac ?(local = false) isrec tactics =
     in
     List.iter iter defs
 
-let register_type ?(local = false) isrec types =
+let qualid_to_ident (loc, qid) =
+  let (dp, id) = Libnames.repr_qualid qid in
+  if DirPath.is_empty dp then (loc, id)
+  else user_err ~loc (str "Identifier expected")
+
+let register_typedef ?(local = false) isrec types =
   let same_name ((_, id1), _) ((_, id2), _) = Id.equal id1 id2 in
   let () = match List.duplicates same_name types with
   | [] -> ()
@@ -242,6 +327,10 @@ let register_type ?(local = false) isrec types =
         user_err (str "Multiple definitions of the projection " ++ Id.print id)
       in
       ()
+    | CTydOpn ->
+      if isrec then
+        user_err ~loc (str "The open type declaration " ++ Id.print id ++
+          str " cannot be recursive")
   in
   let () = List.iter check types in
   let self =
@@ -289,6 +378,63 @@ let register_primitive ?(local = false) (loc, id) t ml =
   } in
   ignore (Lib.add_leaf id (inTacDef def))
 
+let register_open ?(local = false) (loc, qid) (params, def) =
+  let kn =
+    try Tac2env.locate_type qid
+    with Not_found ->
+      user_err ~loc (str "Unbound type " ++ pr_qualid qid)
+  in
+  let (tparams, t) = Tac2env.interp_type kn in
+  let () = match t with
+  | GTydOpn -> ()
+  | GTydAlg _ | GTydRec _ | GTydDef _ ->
+    user_err ~loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
+  in
+  let () =
+    if not (Int.equal (List.length params) tparams) then
+      Tac2intern.error_nparams_mismatch loc (List.length params) tparams
+  in
+  match def with
+  | CTydOpn -> ()
+  | CTydAlg def ->
+    let intern_type t =
+      let tpe = CTydDef (Some t) in
+      let (_, ans) = intern_typedef Id.Map.empty (params, tpe) in
+      match ans with
+      | GTydDef (Some t) -> t
+      | _ -> assert false
+    in
+    let map (id, tpe) =
+      let tpe = List.map intern_type tpe in
+      { edata_name = id; edata_args = tpe }
+    in
+    let def = List.map map def in
+    let def = {
+      typext_local = local;
+      typext_type = kn;
+      typext_prms = tparams;
+      typext_expr = def;
+    } in
+    Lib.add_anonymous_leaf (inTypExt def)
+  | CTydRec _ | CTydDef _ ->
+    user_err ~loc (str "Extensions only accept inductive constructors")
+
+let register_type ?local isrec types = match types with
+| [qid, true, def] ->
+  let (loc, _) = qid in
+  let () = if isrec then user_err ~loc (str "Extensions cannot be recursive") in
+  register_open ?local qid def
+| _ ->
+  let map (qid, redef, def) =
+    let (loc, _) = qid in
+    let () = if redef then
+      user_err ~loc (str "Types can only be extended one by one")
+    in
+    (qualid_to_ident qid, def)
+  in
+  let types = List.map map types in
+  register_typedef ?local isrec types
+
 let register_struct ?local str = match str with
 | StrVal (isrec, e) -> register_ltac ?local isrec e
 | StrTyp (isrec, t) -> register_type ?local isrec t
diff --git a/tac2entries.mli b/tac2entries.mli
index 9c5d0a15fd..0d9b3ad134 100644
--- a/tac2entries.mli
+++ b/tac2entries.mli
@@ -8,6 +8,7 @@
 
 open Loc
 open Names
+open Libnames
 open Tac2expr
 
 (** {5 Toplevel definitions} *)
@@ -16,7 +17,7 @@ val register_ltac : ?local:bool -> rec_flag ->
   (Name.t located * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
-  (Id.t located * raw_quant_typedef) list -> unit
+  (qualid located * redef_flag * raw_quant_typedef) list -> unit
 
 val register_primitive : ?local:bool ->
   Id.t located -> raw_typexpr -> ml_tactic_name -> unit
diff --git a/tac2env.ml b/tac2env.ml
index 5e379473c8..0fcdba1ca7 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -22,7 +22,7 @@ type constructor_data = {
   cdata_prms : int;
   cdata_type : type_constant;
   cdata_args : int glb_typexpr list;
-  cdata_indx : int;
+  cdata_indx : int option;
 }
 
 type projection_data = {
@@ -62,8 +62,9 @@ let rec eval_pure = function
   ValCls { clos_env = Id.Map.empty; clos_var = na; clos_exp = e }
 | GTacCst (_, n, []) -> ValInt n
 | GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
+| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_pure el)
 | GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _
-| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ ->
+| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 
 let define_global kn e =
diff --git a/tac2env.mli b/tac2env.mli
index 16232ec810..477f4ebec7 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -33,10 +33,11 @@ type constructor_data = {
   (** Inductive definition to which the constructor pertains *)
   cdata_args : int glb_typexpr list;
   (** Types of the constructor arguments *)
-  cdata_indx : int;
+  cdata_indx : int option;
   (** Index of the constructor in the ADT. Numbering is duplicated between
       argumentless and argument-using constructors, e.g. in type ['a option]
-      [None] and [Some] have both index 0. *)
+      [None] and [Some] have both index 0. This field is empty whenever the
+      constructor is a member of an open type. *)
 }
 
 val define_constructor : ltac_constructor -> constructor_data -> unit
diff --git a/tac2expr.mli b/tac2expr.mli
index 1fac5a2315..1840b567b4 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -13,6 +13,7 @@ open Libnames
 
 type mutable_flag = bool
 type rec_flag = bool
+type redef_flag = bool
 type lid = Id.t
 type uid = Id.t
 
@@ -40,6 +41,7 @@ type raw_typedef =
 | CTydDef of raw_typexpr option
 | CTydAlg of (uid * raw_typexpr list) list
 | CTydRec of (lid * mutable_flag * raw_typexpr) list
+| CTydOpn
 
 type 'a glb_typexpr =
 | GTypVar of 'a
@@ -51,6 +53,7 @@ type glb_typedef =
 | GTydDef of int glb_typexpr option
 | GTydAlg of (uid * int glb_typexpr list) list
 | GTydRec of (lid * mutable_flag * int glb_typexpr) list
+| GTydOpn
 
 type type_scheme = int * int glb_typexpr
 
@@ -94,6 +97,13 @@ type case_info =
 | GCaseTuple of int
 | GCaseAlg of type_constant
 
+type 'a open_match = {
+  opn_match : 'a;
+  opn_branch : (Name.t * Name.t array * 'a) KNmap.t;
+  (** Invariant: should not be empty *)
+  opn_default : Name.t * 'a;
+}
+
 type glb_tacexpr =
 | GTacAtm of atom
 | GTacVar of Id.t
@@ -106,22 +116,27 @@ type glb_tacexpr =
 | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
 | GTacPrj of type_constant * glb_tacexpr * int
 | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
+| GTacOpn of ltac_constructor * glb_tacexpr list
+| GTacWth of glb_tacexpr open_match
 | GTacExt of glob_generic_argument
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
 (** Toplevel statements *)
 type strexpr =
 | StrVal of rec_flag * (Name.t located * raw_tacexpr) list
-| StrTyp of rec_flag * (Id.t located * raw_quant_typedef) list
+  (** Term definition *)
+| StrTyp of rec_flag * (qualid located * redef_flag * raw_quant_typedef) list
+  (** Type definition *)
 | StrPrm of Id.t located * raw_typexpr * ml_tactic_name
+  (** External definition *)
 
 (** {5 Dynamic semantics} *)
 
 (** Values are represented in a way similar to OCaml, i.e. they constrast
     immediate integers (integers, constructors without arguments) and structured
     blocks (tuples, arrays, constructors with arguments), as well as a few other
-    base cases, namely closures, strings and dynamic type coming from the Coq
-    implementation. *)
+    base cases, namely closures, strings, named constructors, and dynamic type
+    coming from the Coq implementation. *)
 
 type tag = int
 
@@ -134,6 +149,8 @@ type valexpr =
   (** Strings *)
 | ValCls of closure
   (** Closures *)
+| ValOpn of KerName.t * valexpr array
+  (** Open constructors *)
 | ValExt of Geninterp.Val.t
   (** Arbitrary data *)
 
diff --git a/tac2intern.ml b/tac2intern.ml
index c4d2fc277b..32d1e07c17 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -215,6 +215,11 @@ let error_nargs_mismatch loc nargs nfound =
     str " arguments, but is applied to " ++ int nfound ++
     str " arguments")
 
+let error_nparams_mismatch loc nargs nfound =
+  user_err ~loc (str "Type expects " ++ int nargs ++
+    str " arguments, but is applied to " ++ int nfound ++
+    str " arguments")
+
 let rec subst_type subst (t : 'a glb_typexpr) = match t with
 | GTypVar id -> subst id
 | GTypArrow (t1, t2) -> GTypArrow (subst_type subst t1, subst_type subst t2)
@@ -275,7 +280,7 @@ let fresh_reftype env (kn : KerName.t) =
 
 let is_unfoldable kn = match snd (Tac2env.interp_type kn) with
 | GTydDef (Some _) -> true
-| GTydDef None | GTydAlg _ | GTydRec _ -> false
+| GTydDef None | GTydAlg _ | GTydRec _ | GTydOpn -> false
 
 let unfold env kn args =
   let (nparams, def) = Tac2env.interp_type kn in
@@ -349,7 +354,7 @@ let unify loc env t1 t2 =
 
 let is_pure_constructor kn =
   match snd (Tac2env.interp_type kn) with
-  | GTydAlg _ -> true
+  | GTydAlg _ | GTydOpn -> true
   | GTydRec fields ->
     let is_pure (_, mut, _) = not mut in
     List.for_all is_pure fields
@@ -360,14 +365,16 @@ let rec is_value = function
 | GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
 | GTacCst (GCaseTuple _, _, el) -> List.for_all is_value el
 | GTacCst (_, _, []) -> true
+| GTacOpn (_, el) -> List.for_all is_value el
 | GTacCst (GCaseAlg kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
-| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ -> false
+| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
+| GTacWth _ -> false
 
 let is_rec_rhs = function
 | GTacFun _ -> true
 | GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _
 | GTacSet _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _
-| GTacCse _ -> false
+| GTacCse _ | GTacOpn _ | GTacWth _ -> false
 
 let rec fv_type f t accu = match t with
 | GTypVar id -> f id accu
@@ -503,40 +510,55 @@ let invalid_pattern ~loc kn t =
   user_err ~loc (str "Invalid pattern, expected a pattern for type " ++
     pr_typref kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
 
+(** Pattern view *)
+
+type glb_patexpr =
+| GPatVar of Name.t
+| GPatRef of ltac_constructor * glb_patexpr list
+| GPatTup of glb_patexpr list
+
+let rec intern_patexpr env = function
+| CPatAny _ -> GPatVar Anonymous
+| CPatRef (_, qid, []) ->
+  begin match get_constructor env qid with
+  | ArgVar (_, id) -> GPatVar (Name id)
+  | ArgArg (_, kn) -> GPatRef (kn, [])
+  end
+| CPatRef (_, qid, pl) ->
+  begin match get_constructor env qid with
+  | ArgVar (loc, _) ->
+    user_err ~loc (str "Unbound constructor " ++ pr_qualid (snd qid))
+  | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
+  end
+| CPatTup (_, pl) ->
+  GPatTup (List.map (fun p -> intern_patexpr env p) pl)
+
 type pattern_kind =
 | PKind_empty
-| PKind_variant of KerName.t
+| PKind_variant of type_constant
+| PKind_open of type_constant
 | PKind_tuple of int
 | PKind_any
 
 let get_pattern_kind env pl = match pl with
 | [] -> PKind_empty
 | p :: pl ->
-  let rec get_kind p pl = match fst p with
-  | CPatAny _ ->
+  let rec get_kind (p, _) pl = match intern_patexpr env p with
+  | GPatVar _ ->
     begin match pl with
     | [] -> PKind_any
     | p :: pl -> get_kind p pl
     end
-  | CPatRef (_, qid, []) ->
-    begin match get_constructor env qid with
-    | ArgVar _ ->
-      begin match pl with
-      | [] -> PKind_any
-      | p :: pl -> get_kind p pl
-      end
-    | ArgArg (data, _) -> PKind_variant data.cdata_type
-    end
-  | CPatRef (_, qid, _ :: _) ->
-    begin match get_constructor env qid with
-    | ArgVar (loc, _) ->
-      user_err ~loc (str "Unbound constructor " ++ pr_qualid (snd qid))
-    | ArgArg (data, _) -> PKind_variant data.cdata_type
-    end
-  | CPatTup (_, tp) -> PKind_tuple (List.length tp)
+  | GPatRef (kn, pl) ->
+    let data = Tac2env.interp_constructor kn in
+    if Option.is_empty data.cdata_indx then PKind_open data.cdata_type
+    else PKind_variant data.cdata_type
+  | GPatTup tp -> PKind_tuple (List.length tp)
   in
   get_kind p pl
 
+(** Internalization *)
+
 let is_constructor env qid = match get_variable env qid with
 | ArgArg (TacConstructor _) -> true
 | _ -> false
@@ -739,9 +761,8 @@ and intern_case env loc e pl =
   match get_pattern_kind env pl with
   | PKind_any ->
     let (pat, b) = List.hd pl in
-    let na = match pat with
-    | CPatAny _ -> Anonymous
-    | CPatRef (_, (_, qid), _) -> Name (snd (repr_qualid qid))
+    let na = match intern_patexpr env pat with
+    | GPatVar na -> na
     | _ -> assert false
     in
     let () = check_redundant_clause (List.tl pl) in
@@ -851,7 +872,10 @@ and intern_case env loc e pl =
         let nenv = List.fold_left2 fold env ids data.cdata_args in
         let (br', brT) = intern_rec nenv br in
         let () =
-          let index = data.cdata_indx in
+          let index = match data.cdata_indx with
+          | Some i -> i
+          | None -> assert false
+          in
           if List.is_empty args then
             if Option.is_empty const.(index) then const.(index) <- Some br'
             else warn_redundant_clause ~loc ()
@@ -869,13 +893,67 @@ and intern_case env loc e pl =
     in
     let () = intern_branch pl in
     let map = function
-    | None -> user_err ~loc (str "Unhandled match case") (** FIXME *)
+    | None -> user_err ~loc (str "TODO: Unhandled match case") (** FIXME *)
     | Some x -> x
     in
     let const = Array.map map const in
     let nonconst = Array.map map nonconst in
     let ce = GTacCse (e', GCaseAlg kn, const, nonconst) in
     (ce, ret)
+  | PKind_open kn ->
+    let subst, tc = fresh_reftype env kn in
+    let () = unify (loc_of_tacexpr e) env t tc in
+    let ret = GTypVar (fresh_id env) in
+    let rec intern_branch map = function
+    | [] ->
+      user_err ~loc (str "Missing default case")
+    | (pat, br) :: rem ->
+      match intern_patexpr env pat with
+      | GPatVar na ->
+        let () = check_redundant_clause rem in
+        let nenv = push_name na (monomorphic tc) env in
+        let br' = intern_rec_with_constraint nenv br ret in
+        let def = (na, br') in
+        (map, def)
+      | GPatRef (knc, args) ->
+        let get = function
+        | GPatVar na -> na
+        | GPatRef _ | GPatTup _ ->
+          user_err ~loc (str "TODO: Unhandled match case") (** FIXME *)
+        in
+        let loc = loc_of_patexpr pat in
+        let ids = List.map get args in
+        let data = Tac2env.interp_constructor knc in
+        let () =
+          if not (KerName.equal kn data.cdata_type) then
+            invalid_pattern ~loc kn (GCaseAlg data.cdata_type)
+        in
+        let nids = List.length ids in
+        let nargs = List.length data.cdata_args in
+        let () =
+          if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids
+        in
+        let fold env id tpe =
+          (** Instantiate all arguments *)
+          let subst n = GTypVar subst.(n) in
+          let tpe = subst_type subst tpe in
+          push_name id (monomorphic tpe) env
+        in
+        let nenv = List.fold_left2 fold env ids data.cdata_args in
+        let br' = intern_rec_with_constraint nenv br ret in
+        let map =
+          if KNmap.mem knc map then
+            let () = warn_redundant_clause ~loc () in
+            map
+          else
+            KNmap.add knc (Anonymous, Array.of_list ids, br') map
+        in
+        intern_branch map rem
+      | GPatTup tup ->
+        invalid_pattern ~loc kn (GCaseTuple (List.length tup))
+    in
+    let (map, def) = intern_branch KNmap.empty pl in
+    (GTacWth { opn_match = e'; opn_branch = map; opn_default = def }, ret)
 
 and intern_constructor env loc kn args =
   let cstr = interp_constructor kn in
@@ -887,7 +965,11 @@ and intern_constructor env loc kn args =
     let ans = GTypRef (cstr.cdata_type, List.init cstr.cdata_prms (fun i -> GTypVar subst.(i))) in
     let map arg tpe = intern_rec_with_constraint env arg tpe in
     let args = List.map2 map args types in
-    (GTacCst (GCaseAlg cstr.cdata_type, cstr.cdata_indx, args), ans)
+    match cstr.cdata_indx with
+    | Some idx ->
+      (GTacCst (GCaseAlg cstr.cdata_type, idx, args), ans)
+    | None ->
+      (GTacOpn (kn, args), ans)
   else
     error_nargs_mismatch loc nargs (List.length args)
 
@@ -986,6 +1068,7 @@ let intern_typedef self (ids, t) : glb_quant_typedef =
     let map (c, mut, t) = (c, mut, intern t) in
     let fields = List.map map fields in
     (count, GTydRec fields)
+  | CTydOpn -> (count, GTydOpn)
 
 let intern_open_type t =
   let env = empty_env () in
@@ -1045,6 +1128,18 @@ let rec subst_expr subst e = match e with
   let cse1' = Array.map (fun (ids, e) -> (ids, subst_expr subst e)) cse1 in
   let ci' = subst_case_info subst ci in
   GTacCse (subst_expr subst e, ci', cse0', cse1')
+| GTacWth { opn_match = e; opn_branch = br; opn_default = (na, def) } as e0 ->
+  let e' = subst_expr subst e in
+  let def' = subst_expr subst def in
+  let fold kn (self, vars, p) accu =
+    let kn' = subst_kn subst kn in
+    let p' = subst_expr subst p in
+    if kn' == kn && p' == p then accu
+    else KNmap.add kn' (self, vars, p') (KNmap.remove kn accu)
+  in
+  let br' = KNmap.fold fold br br in
+  if e' == e && br' == br && def' == def then e0
+  else GTacWth { opn_match = e'; opn_default = (na, def'); opn_branch = br' }
 | GTacPrj (kn, e, p) as e0 ->
   let kn' = subst_kn subst kn in
   let e' = subst_expr subst e in
@@ -1057,6 +1152,10 @@ let rec subst_expr subst e = match e with
 | GTacExt ext ->
   let ext' = Genintern.generic_substitute subst ext in
   if ext' == ext then e else GTacExt ext'
+| GTacOpn (kn, el) as e0 ->
+  let kn' = subst_kn subst kn in
+  let el' = List.smartmap (fun e -> subst_expr subst e) el in
+  if kn' == kn && el' == el then e0 else GTacOpn (kn', el')
 
 let subst_typedef subst e = match e with
 | GTydDef t ->
@@ -1076,6 +1175,7 @@ let subst_typedef subst e = match e with
   in
   let fields' = List.smartmap map fields in
   if fields' == fields then e else GTydRec fields'
+| GTydOpn -> GTydOpn
 
 let subst_quant_typedef subst (prm, def as qdef) =
   let def' = subst_typedef subst def in
diff --git a/tac2intern.mli b/tac2intern.mli
index 6633792e7e..4c482d0b0c 100644
--- a/tac2intern.mli
+++ b/tac2intern.mli
@@ -26,3 +26,8 @@ val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr
 val subst_expr : substitution -> glb_tacexpr -> glb_tacexpr
 val subst_quant_typedef : substitution -> glb_quant_typedef -> glb_quant_typedef
 val subst_type_scheme : substitution -> type_scheme -> type_scheme
+
+(** Errors *)
+
+val error_nargs_mismatch : Loc.t -> int -> int -> 'a
+val error_nparams_mismatch : Loc.t -> int -> int -> 'a
diff --git a/tac2interp.ml b/tac2interp.ml
index cd307e3ae7..664b7de3d6 100644
--- a/tac2interp.ml
+++ b/tac2interp.ml
@@ -14,7 +14,14 @@ open Names
 open Proofview.Notations
 open Tac2expr
 
-exception LtacError of KerName.t * valexpr
+exception LtacError of KerName.t * valexpr array
+
+let () = register_handler begin function
+| LtacError (kn, _) ->
+  let c = Tac2print.pr_constructor kn in
+  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
+| _ -> raise Unhandled
+end
 
 let val_exn = Geninterp.Val.create "ltac2:exn"
 
@@ -81,12 +88,17 @@ let rec interp ist = function
   return (ValBlk (n, Array.of_list el))
 | GTacCse (e, _, cse0, cse1) ->
   interp ist e >>= fun e -> interp_case ist e cse0 cse1
+| GTacWth { opn_match = e; opn_branch = cse; opn_default = def } ->
+  interp ist e >>= fun e -> interp_with ist e cse def
 | GTacPrj (_, e, p) ->
   interp ist e >>= fun e -> interp_proj ist e p
 | GTacSet (_, e, p, r) ->
   interp ist e >>= fun e ->
   interp ist r >>= fun r ->
   interp_set ist e p r
+| GTacOpn (kn, el) ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  return (ValOpn (kn, Array.of_list el))
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   Tac2env.interp_primitive ml el
@@ -106,7 +118,7 @@ and interp_app f args = match f with
   | id :: ids, arg :: args -> push (push_name ist id arg) ids args
   in
   push ist ids args
-| ValExt _ | ValInt _ | ValBlk _ | ValStr _ ->
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
 
 and interp_case ist e cse0 cse1 = match e with
@@ -115,18 +127,34 @@ and interp_case ist e cse0 cse1 = match e with
   let (ids, e) = cse1.(n) in
   let ist = CArray.fold_left2 push_name ist ids args in
   interp ist e
-| ValExt _ | ValStr _ | ValCls _ ->
+| ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
+  anomaly (str "Unexpected value shape")
+
+and interp_with ist e cse def = match e with
+| ValOpn (kn, args) ->
+  let br = try Some (KNmap.find kn cse) with Not_found -> None in
+  begin match br with
+  | None ->
+    let (self, def) = def in
+    let ist = push_name ist self e in
+    interp ist def
+  | Some (self, ids, p) ->
+    let ist = push_name ist self e in
+    let ist = CArray.fold_left2 push_name ist ids args in
+    interp ist p
+  end
+| ValInt _ | ValBlk _ | ValExt _ | ValStr _ | ValCls _ ->
   anomaly (str "Unexpected value shape")
 
 and interp_proj ist e p = match e with
 | ValBlk (_, args) ->
   return args.(p)
-| ValInt _ | ValExt _ | ValStr _ | ValCls _ ->
+| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
 
 and interp_set ist e p r = match e with
 | ValBlk (_, args) ->
   let () = args.(p) <- r in
   return (ValInt 0)
-| ValInt _ | ValExt _ | ValStr _ | ValCls _ ->
+| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
diff --git a/tac2interp.mli b/tac2interp.mli
index 7fe78a9460..bf6b2d4dde 100644
--- a/tac2interp.mli
+++ b/tac2interp.mli
@@ -20,8 +20,9 @@ val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic
 
 (** {5 Exceptions} *)
 
-exception LtacError of KerName.t * valexpr
-(** Ltac2-defined exceptions *)
+exception LtacError of KerName.t * valexpr array
+(** Ltac2-defined exceptions seen from OCaml side *)
 
 val val_exn : Exninfo.iexn Geninterp.Val.typ
-(** Toplevel representation of Ltac2 exceptions *)
+(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
+    should be put into a value with tag [val_exn]. *)
diff --git a/tac2print.ml b/tac2print.ml
index a7f9ed48c8..ffa5ddc05a 100644
--- a/tac2print.ml
+++ b/tac2print.ml
@@ -153,7 +153,7 @@ let pr_glbexpr_gen lvl c =
     | E0 -> paren
     | E1 | E2 | E3 | E4 | E5 -> fun x -> x
     in
-    paren (pr_glbexpr E1 c) ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)
+    paren (pr_glbexpr E1 c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))
   | GTacLet (mut, bnd, e) ->
     let paren = match lvl with
     | E0 | E1 | E2 | E3 | E4 -> paren
@@ -195,7 +195,7 @@ let pr_glbexpr_gen lvl c =
       in
       let args = prlist_with_sep (fun () -> str ";" ++ spc ()) pr_arg args in
       str "{" ++ spc () ++ args ++ spc () ++ str "}"
-    | _, GTydDef _ -> assert false
+    | _, (GTydDef _ | GTydOpn) -> assert false
     end
   | GTacCse (e, info, cst_br, ncst_br) ->
     let e = pr_glbexpr E5 e in
@@ -203,7 +203,7 @@ let pr_glbexpr_gen lvl c =
     | GCaseAlg kn ->
       let def = match Tac2env.interp_type kn with
       | _, GTydAlg def -> def
-      | _, GTydDef _ | _, GTydRec _ -> assert false
+      | _, GTydDef _ | _, GTydRec _ | _, GTydOpn -> assert false
       in
       let br = order_branches cst_br ncst_br def in
       let pr_branch (cstr, vars, p) =
@@ -224,10 +224,33 @@ let pr_glbexpr_gen lvl c =
       str "|" ++ spc () ++ paren vars ++ spc () ++ str "=>" ++ spc () ++ p
     in
     hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end")
+  | GTacWth wth ->
+    let e = pr_glbexpr E5 wth.opn_match in
+    let pr_pattern c self vars p =
+      let self = match self with
+      | Anonymous -> mt ()
+      | Name id -> spc () ++ str "as" ++ spc () ++ Id.print id
+      in
+      hov 0 (str "|" ++ spc () ++ c ++ vars ++ self ++ spc () ++ str "=>" ++ spc () ++
+        hov 2 (pr_glbexpr E5 p)) ++ spc ()
+    in
+    let pr_branch (cstr, (self, vars, p)) =
+      let cstr = pr_constructor cstr in
+      let vars = match Array.to_list vars with
+      | [] -> mt ()
+      | vars -> spc () ++ pr_sequence pr_name vars
+      in
+      pr_pattern cstr self vars p
+    in
+    let br = prlist pr_branch (KNmap.bindings wth.opn_branch) in
+    let (def_as, def_p) = wth.opn_default in
+    let def = pr_pattern (str "_") def_as (mt ()) def_p in
+    let br = br ++ def in
+    hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end")
   | GTacPrj (kn, e, n) ->
     let def = match Tac2env.interp_type kn with
     | _, GTydRec def -> def
-    | _, GTydDef _ | _, GTydAlg _ -> assert false
+    | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
     in
     let (proj, _, _) = List.nth def n in
     let proj = change_kn_label kn proj in
@@ -237,7 +260,7 @@ let pr_glbexpr_gen lvl c =
   | GTacSet (kn, e, n, r) ->
     let def = match Tac2env.interp_type kn with
     | _, GTydRec def -> def
-    | _, GTydDef _ | _, GTydAlg _ -> assert false
+    | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
     in
     let (proj, _, _) = List.nth def n in
     let proj = change_kn_label kn proj in
@@ -245,6 +268,13 @@ let pr_glbexpr_gen lvl c =
     let e = pr_glbexpr E0 e in
     let r = pr_glbexpr E1 r in
     e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r
+  | GTacOpn (kn, cl) ->
+    let paren = match lvl with
+    | E0 -> paren
+    | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    let c = pr_constructor kn in
+    paren (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))
   | GTacExt arg ->
     let GenArg (Glbwit tag, arg) = arg in
     let name = match tag with