Proper handling of record types.

We add the standard ML facilities for records, that is, projections,
mutable fields and primitive to set them.

8 files changed, 360 insertions, 80 deletions

diff --git a/Ltac2.v b/Ltac2.v
index a952524e71..0933c1e0b4 100644
--- a/Ltac2.v
+++ b/Ltac2.v
@@ -20,7 +20,7 @@ Ltac2 Type 'a array.
 
 (** Pervasive types *)
 
-Ltac2 Type 'a option := | None | Some ('a).
+Ltac2 Type 'a option := [ None | Some ('a) ].
 
 (** Primitive tactics *)
 
diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index b613f22a8d..ce2becd9f9 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -50,6 +50,8 @@ GEXTEND Gram
       [ e1 = tac2expr; ";"; e2 = tac2expr -> CTacSeq (!@loc, e1, e2) ]
     | "1" LEFTA
       [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
+      | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, qid)
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, qid, r)
       | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "0" SEP "," -> CTacTup (!@loc, e0 :: el) ]
     | "0"
       [ "("; a = tac2expr LEVEL "5"; ")" -> a
@@ -57,6 +59,7 @@ GEXTEND Gram
       | "()" -> CTacTup (!@loc, [])
       | "("; ")" -> CTacTup (!@loc, [])
       | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (!@loc, a)
+      | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a)
       | a = tactic_atom -> a ]
     ]
   ;
@@ -126,16 +129,35 @@ GEXTEND Gram
   ;
   tac2typ_knd:
     [ [ t = tac2type -> CTydDef (Some t)
-      | t = tac2alg_type -> CTydAlg t ] ]
+      | "["; t = tac2alg_constructors; "]" -> CTydAlg t
+      | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ]
   ;
-  tac2alg_type:
-    [ [ -> []
-      | "|"; bl = LIST1 tac2alg_constructor SEP "|" -> bl ] ]
+  tac2alg_constructors:
+    [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> cs
+      | cs = LIST0 tac2alg_constructor SEP "|" -> cs ] ]
   ;
   tac2alg_constructor:
     [ [ c = Prim.ident -> (c, [])
       | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ]
   ;
+  tac2rec_fields:
+    [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> f :: l
+      | f = tac2rec_field; ";" -> [f]
+      | f = tac2rec_field -> [f]
+      | -> [] ] ]
+  ;
+  tac2rec_field:
+    [ [ mut = [ -> false | IDENT "mutable" -> true]; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
+  ;
+  tac2rec_fieldexprs:
+    [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l
+      | f = tac2rec_fieldexpr; ";" -> [f]
+      | f = tac2rec_fieldexpr-> [f]
+      | -> [] ] ]
+  ;
+  tac2rec_fieldexpr:
+    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> qid, e ] ]
+  ;
   tac2typ_prm:
     [ [ -> []
       | id = typ_param -> [!@loc, id]
diff --git a/tac2entries.ml b/tac2entries.ml
index 7572270ab3..4098324f12 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -13,6 +13,7 @@ open Names
 open Libnames
 open Libobject
 open Nametab
+open Tac2env
 open Tac2expr
 open Tac2intern
 open Vernacexpr
@@ -24,14 +25,14 @@ type tacdef = {
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
-  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in
+  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let load_tacdef i obj = perform_tacdef (Until i) obj
 let open_tacdef i obj = perform_tacdef (Exactly i) obj
 
 let cache_tacdef ((sp, kn), def) =
-  let () = Tac2env.push_ltac (Until 1) sp kn in
+  let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let subst_tacdef (subst, def) =
@@ -71,12 +72,19 @@ let push_typedef visibility sp kn (_, def) = match def with
   let iter (c, _) =
     let spc = change_sp_label sp c in
     let knc = change_kn_label kn c in
-    Tac2env.push_ltac visibility spc knc
+    Tac2env.push_ltac visibility spc (TacConstructor knc)
   in
   Tac2env.push_type visibility sp kn;
   List.iter iter cstrs
-| GTydRec _ ->
-  assert false (** FIXME *)
+| GTydRec fields ->
+  (** Register fields *)
+  let iter (c, _, _) =
+    let spc = change_sp_label sp c in
+    let knc = change_kn_label kn c in
+    Tac2env.push_projection visibility spc knc
+  in
+  Tac2env.push_type visibility sp kn;
+  List.iter iter fields
 
 let next i =
   let ans = !i in
@@ -95,27 +103,31 @@ let define_typedef kn (params, def as qdef) = match def with
   let iter (c, args) =
     let knc = change_kn_label kn c in
     let tag = if List.is_empty args then next constant else next nonconstant in
-    let ids = List.mapi (fun i _ -> dummy_var i) args in
-    let c = GTacCst (kn, tag, List.map (fun id -> GTacVar id) ids) in
-    let c =
-      if List.is_empty args then c
-      else GTacFun (List.map (fun id -> Name id) ids, c)
-    in
-    let fold arg tpe = GTypArrow (arg, tpe) in
-    let cT = GTypRef (kn, List.init params (fun i -> GTypVar i)) in
-    let cT = List.fold_right fold args cT in
     let data = {
-      Tac2env.cdata_type = kn;
-      cdata_args = params, args;
+      Tac2env.cdata_prms = params;
+      cdata_type = kn;
+      cdata_args = args;
       cdata_indx = tag;
     } in
-    Tac2env.define_constructor knc data;
-    Tac2env.define_global knc (c, (params, cT))
+    Tac2env.define_constructor knc data
   in
   Tac2env.define_type kn qdef;
   List.iter iter cstrs
-| GTydRec _ ->
-  assert false (** FIXME *)
+| GTydRec fs ->
+  (** Define projections *)
+  let iter i (id, mut, t) =
+    let knp = change_kn_label kn id in
+    let proj = {
+      Tac2env.pdata_prms = params;
+      pdata_type = kn;
+      pdata_ptyp = t;
+      pdata_mutb = mut;
+      pdata_indx = i;
+    } in
+    Tac2env.define_projection knp proj
+  in
+  Tac2env.define_type kn qdef;
+  List.iteri iter fs
 
 let perform_typdef vs ((sp, kn), def) =
   let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in
@@ -213,8 +225,22 @@ let register_type ?(local = false) isrec types =
       if isrec then
         user_err ~loc (str "The type abbreviation " ++ Id.print id ++
           str " cannot be recursive")
-    | CTydAlg _ -> () (** FIXME *)
-    | CTydRec _ -> assert false (** FIXME *)
+    | CTydAlg cs ->
+      let same_name (id1, _) (id2, _) = Id.equal id1 id2 in
+      let () = match List.duplicates same_name cs with
+      | [] -> ()
+      | (id, _) :: _ ->
+        user_err (str "Multiple definitions of the constructor " ++ Id.print id)
+      in
+      ()
+    | CTydRec ps ->
+      let same_name (id1, _, _) (id2, _, _) = Id.equal id1 id2 in
+      let () = match List.duplicates same_name ps with
+      | [] -> ()
+      | (id, _, _) :: _ ->
+        user_err (str "Multiple definitions of the projection " ++ Id.print id)
+      in
+      ()
   in
   let () = List.iter check types in
   let self =
@@ -275,8 +301,13 @@ let print_ltac ref =
     try Tac2env.locate_ltac qid
     with Not_found -> user_err ~loc (str "Unknown tactic " ++ pr_qualid qid)
   in
-  let (_, (_, t)) = Tac2env.interp_global kn in
-  Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t)
+  match kn with
+  | TacConstant kn ->
+    let (_, (_, t)) = Tac2env.interp_global kn in
+    Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t)
+  | TacConstructor kn ->
+    let _ = Tac2env.interp_constructor kn in
+    Feedback.msg_notice (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid)
 
 (** Calling tactics *)
 
diff --git a/tac2env.ml b/tac2env.ml
index 3500b2ef3d..bdb8f41ef8 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -15,23 +15,35 @@ open Tac2expr
 
 type ltac_constant = KerName.t
 type ltac_constructor = KerName.t
+type ltac_projection = KerName.t
 type type_constant = KerName.t
 
 type constructor_data = {
+  cdata_prms : int;
   cdata_type : type_constant;
-  cdata_args : int * int glb_typexpr list;
+  cdata_args : int glb_typexpr list;
   cdata_indx : int;
 }
 
+type projection_data = {
+  pdata_prms : int;
+  pdata_type : type_constant;
+  pdata_ptyp : int glb_typexpr;
+  pdata_mutb : bool;
+  pdata_indx : int;
+}
+
 type ltac_state = {
   ltac_tactics : (glb_tacexpr * type_scheme) KNmap.t;
   ltac_constructors : constructor_data KNmap.t;
+  ltac_projections : projection_data KNmap.t;
   ltac_types : glb_quant_typedef KNmap.t;
 }
 
 let empty_state = {
   ltac_tactics = KNmap.empty;
   ltac_constructors = KNmap.empty;
+  ltac_projections = KNmap.empty;
   ltac_types = KNmap.empty;
 }
 
@@ -51,8 +63,8 @@ let rec eval_pure = function
 | GTacTup el -> ValBlk (0, Array.map_of_list eval_pure el)
 | GTacCst (_, n, []) -> ValInt n
 | GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
-| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _
-| GTacApp _ | GTacCse _ | GTacPrm _ | GTacExt _ ->
+| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _
+| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 
 let define_global kn e =
@@ -69,6 +81,12 @@ let define_constructor kn t =
 
 let interp_constructor kn = KNmap.find kn ltac_state.contents.ltac_constructors
 
+let define_projection kn t =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_projections = KNmap.add kn t state.ltac_projections }
+
+let interp_projection kn = KNmap.find kn ltac_state.contents.ltac_projections
+
 let define_type kn e =
   let state = !ltac_state in
   ltac_state := { state with ltac_types = KNmap.add kn e state.ltac_types }
@@ -103,28 +121,47 @@ struct
     id, (DirPath.repr dir)
 end
 
+type tacref =
+| TacConstant of ltac_constant
+| TacConstructor of ltac_constructor
+
+module TacRef =
+struct
+type t = tacref
+let equal r1 r2 = match r1, r2 with
+| TacConstant c1, TacConstant c2 -> KerName.equal c1 c2
+| TacConstructor c1, TacConstructor c2 -> KerName.equal c1 c2
+| _ -> false
+end
+
 module KnTab = Nametab.Make(FullPath)(KerName)
+module RfTab = Nametab.Make(FullPath)(TacRef)
 
 type nametab = {
-  tab_ltac : KnTab.t;
+  tab_ltac : RfTab.t;
   tab_type : KnTab.t;
+  tab_proj : KnTab.t;
 }
 
-let empty_nametab = { tab_ltac = KnTab.empty; tab_type = KnTab.empty }
+let empty_nametab = {
+  tab_ltac = RfTab.empty;
+  tab_type = KnTab.empty;
+  tab_proj = KnTab.empty;
+}
 
 let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
 
 let push_ltac vis sp kn =
   let tab = !nametab in
-  nametab := { tab with tab_ltac = KnTab.push vis sp kn tab.tab_ltac }
+  nametab := { tab with tab_ltac = RfTab.push vis sp kn tab.tab_ltac }
 
 let locate_ltac qid =
   let tab = !nametab in
-  KnTab.locate qid tab.tab_ltac
+  RfTab.locate qid tab.tab_ltac
 
 let locate_extended_all_ltac qid =
   let tab = !nametab in
-  KnTab.find_prefixes qid tab.tab_ltac
+  RfTab.find_prefixes qid tab.tab_ltac
 
 let push_type vis sp kn =
   let tab = !nametab in
@@ -138,6 +175,18 @@ let locate_extended_all_type qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_type
 
+let push_projection vis sp kn =
+  let tab = !nametab in
+  nametab := { tab with tab_proj = KnTab.push vis sp kn tab.tab_proj }
+
+let locate_projection qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_proj
+
+let locate_extended_all_projection qid =
+  let tab = !nametab in
+  KnTab.find_prefixes qid tab.tab_proj
+
 type 'a ml_object = {
   ml_type : type_constant;
   ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
diff --git a/tac2env.mli b/tac2env.mli
index eb471b9abf..bcfa70487a 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -14,10 +14,6 @@ open Tac2expr
 
 (** Ltac2 global environment *)
 
-type ltac_constant = KerName.t
-type ltac_constructor = KerName.t
-type type_constant = KerName.t
-
 (** {5 Toplevel definition of values} *)
 
 val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
@@ -31,24 +27,57 @@ val interp_type : type_constant -> glb_quant_typedef
 (** {5 Toplevel definition of algebraic constructors} *)
 
 type constructor_data = {
+  cdata_prms : int;
+  (** Type parameters *)
   cdata_type : type_constant;
-  cdata_args : int * int glb_typexpr list;
+  (** Inductive definition to which the constructor pertains *)
+  cdata_args : int glb_typexpr list;
+  (** Types of the constructor arguments *)
   cdata_indx : int;
+  (** 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. *)
 }
 
 val define_constructor : ltac_constructor -> constructor_data -> unit
 val interp_constructor : ltac_constructor -> constructor_data
 
+(** {5 Toplevel definition of projections} *)
+
+type projection_data = {
+  pdata_prms : int;
+  (** Type parameters *)
+  pdata_type : type_constant;
+  (** Record definition to which the projection pertains *)
+  pdata_ptyp : int glb_typexpr;
+  (** Type of the projection *)
+  pdata_mutb : bool;
+  (** Whether the field is mutable *)
+  pdata_indx : int;
+  (** Index of the projection *)
+}
+
+val define_projection : ltac_projection -> projection_data -> unit
+val interp_projection : ltac_projection -> projection_data
+
 (** {5 Name management} *)
 
-val push_ltac : visibility -> full_path -> ltac_constant -> unit
-val locate_ltac : qualid -> ltac_constant
-val locate_extended_all_ltac : qualid -> ltac_constant list
+type tacref =
+| TacConstant of ltac_constant
+| TacConstructor of ltac_constructor
+
+val push_ltac : visibility -> full_path -> tacref -> unit
+val locate_ltac : qualid -> tacref
+val locate_extended_all_ltac : qualid -> tacref list
 
 val push_type : visibility -> full_path -> type_constant -> unit
 val locate_type : qualid -> type_constant
 val locate_extended_all_type : qualid -> type_constant list
 
+val push_projection : visibility -> full_path -> ltac_projection -> unit
+val locate_projection : qualid -> ltac_projection
+val locate_extended_all_projection : qualid -> ltac_projection list
+
 (** {5 Toplevel definitions of ML tactics} *)
 
 (** This state is not part of the summary, contrarily to the ones above. It is
diff --git a/tac2expr.mli b/tac2expr.mli
index 15c630ca87..b9b649e481 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -16,6 +16,11 @@ type rec_flag = bool
 type lid = Id.t
 type uid = Id.t
 
+type ltac_constant = KerName.t
+type ltac_constructor = KerName.t
+type ltac_projection = KerName.t
+type type_constant = KerName.t
+
 (** {5 Misc} *)
 
 type ml_tactic_name = {
@@ -40,7 +45,7 @@ type 'a glb_typexpr =
 | GTypVar of 'a
 | GTypArrow of 'a glb_typexpr * 'a glb_typexpr
 | GTypTuple of 'a glb_typexpr list
-| GTypRef of KerName.t * 'a glb_typexpr list
+| GTypRef of type_constant * 'a glb_typexpr list
 
 type glb_typedef =
 | GTydDef of int glb_typexpr option
@@ -76,25 +81,32 @@ type raw_tacexpr =
 | CTacCnv of Loc.t * raw_tacexpr * raw_typexpr
 | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
 | CTacCse of Loc.t * raw_tacexpr * raw_taccase list
+| CTacRec of Loc.t * raw_recexpr
+| CTacPrj of Loc.t * raw_tacexpr * qualid located
+| CTacSet of Loc.t * raw_tacexpr * qualid located * raw_tacexpr
 | CTacExt of Loc.t * raw_generic_argument
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
+and raw_recexpr = (qualid located * raw_tacexpr) list
+
 type case_info =
 | GCaseTuple of int
-| GCaseAlg of KerName.t
+| GCaseAlg of type_constant
 
 type glb_tacexpr =
 | GTacAtm of atom
 | GTacVar of Id.t
-| GTacRef of KerName.t
+| GTacRef of ltac_constant
 | GTacFun of Name.t list * glb_tacexpr
 | GTacApp of glb_tacexpr * glb_tacexpr list
 | GTacLet of rec_flag * (Name.t * glb_tacexpr) list * glb_tacexpr
 | GTacTup of glb_tacexpr list
 | GTacArr of glb_tacexpr list
-| GTacCst of KerName.t * int * glb_tacexpr list
+| GTacCst of type_constant * int * glb_tacexpr list
 | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
+| GTacPrj of glb_tacexpr * int
+| GTacSet of glb_tacexpr * int * glb_tacexpr
 | GTacExt of glob_generic_argument
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
diff --git a/tac2intern.ml b/tac2intern.ml
index a554f959a0..10fcde6efa 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -174,6 +174,9 @@ let loc_of_tacexpr = function
 | CTacCnv (loc, _, _) -> loc
 | CTacSeq (loc, _, _) -> loc
 | CTacCse (loc, _, _) -> loc
+| CTacRec (loc, _) -> loc
+| CTacPrj (loc, _, _) -> loc
+| CTacSet (loc, _, _, _) -> loc
 | CTacExt (loc, _) -> loc
 
 let loc_of_patexpr = function
@@ -181,6 +184,11 @@ let loc_of_patexpr = function
 | CPatRef (loc, _, _) -> loc
 | CPatTup (loc, _) -> loc
 
+let error_nargs_mismatch loc nargs nfound =
+  user_err ~loc (str "Constructor 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)
@@ -320,20 +328,27 @@ let unify loc env t1 t2 =
 
 (** Term typing *)
 
+let is_pure_constructor kn =
+  match snd (Tac2env.interp_type kn) with
+  | GTydAlg _ -> true
+  | GTydRec fields ->
+    let is_pure (_, mut, _) = not mut in
+    List.for_all is_pure fields
+  | GTydDef _ -> assert false (** Type definitions have no constructors *)
+
 let rec is_value = function
 | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
 | GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
 | GTacTup el -> List.for_all is_value el
 | GTacCst (_, _, []) -> true
-| GTacCst (kn, n, el) ->
-  (** To be a value, a constructor must be immutable *)
-  assert false (** TODO *)
-| GTacArr _ | GTacCse _ | GTacExt _ | GTacPrm _ -> false
+| GTacCst (kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
+| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ -> false
 
 let is_rec_rhs = function
 | GTacFun _ -> true
-| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ -> false
-| GTacTup _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _ | GTacCse _ -> false
+| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _
+| GTacSet _ | GTacTup _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _
+| GTacCse _ -> false
 
 let rec fv_type f t accu = match t with
 | GTypVar id -> f id accu
@@ -438,18 +453,23 @@ let get_variable env (loc, qid) =
 let get_constructor env (loc, qid) =
   let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
   match c with
-  | Some knc ->
-    let kn =
-      try Tac2env.interp_constructor knc
-      with Not_found ->
-        CErrors.user_err ~loc (str "The term " ++ pr_qualid qid ++
-          str " is not the constructor of an inductive type.")    in
+  | Some (TacConstructor knc) ->
+    let kn = Tac2env.interp_constructor knc in
     ArgArg (kn, knc)
+  | Some (TacConstant _) ->
+    CErrors.user_err ~loc (str "The term " ++ pr_qualid qid ++
+      str " is not the constructor of an inductive type.")
   | None ->
     let (dp, id) = repr_qualid qid in
     if DirPath.is_empty dp then ArgVar (loc, id)
     else CErrors.user_err ~loc (str "Unbound constructor " ++ pr_qualid qid)
 
+let get_projection (loc, qid) =
+  let kn = try Tac2env.locate_projection qid with Not_found ->
+    user_err ~loc (pr_qualid qid ++ str " is not a projection")
+  in
+  Tac2env.interp_projection kn
+
 let intern_atm env = function
 | AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, []))
 | AtmStr s -> (GTacAtm (AtmStr s), GTypRef (t_string, []))
@@ -496,6 +516,10 @@ let get_pattern_kind env pl = match pl with
   in
   get_kind p pl
 
+let is_constructor env qid = match get_variable env qid with
+| ArgArg (TacConstructor _) -> true
+| _ -> false
+
 let rec intern_rec env = function
 | CTacAtm (_, atm) -> intern_atm env atm
 | CTacRef qid ->
@@ -503,9 +527,11 @@ let rec intern_rec env = function
   | ArgVar (_, id) ->
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
-  | ArgArg kn ->
+  | ArgArg (TacConstant kn) ->
     let (_, sch) = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
+  | ArgArg (TacConstructor kn) ->
+    intern_constructor env (fst qid) kn []
   end
 | CTacFun (loc, bnd, e) ->
   let fold (env, bnd, tl) ((_, na), t) =
@@ -520,6 +546,12 @@ let rec intern_rec env = function
   let (e, t) = intern_rec env e in
   let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
   (GTacFun (bnd, e), t)
+| CTacApp (loc, CTacRef qid, args) when is_constructor env qid ->
+  let kn = match get_variable env qid with
+  | ArgArg (TacConstructor kn) -> kn
+  | _ -> assert false
+  in
+  intern_constructor env (fst qid) kn args
 | CTacApp (loc, f, args) ->
   let (f, ft) = intern_rec env f in
   let fold arg (args, t) =
@@ -571,12 +603,7 @@ let rec intern_rec env = function
   (GTacArr [], GTypRef (t_int, [GTypVar id]))
 | CTacArr (loc, e0 :: el) ->
   let (e0, t0) = intern_rec env e0 in
-  let fold e el =
-    let loc = loc_of_tacexpr e in
-    let (e, t) = intern_rec env e in
-    let () = unify loc env t t0 in
-    e :: el
-  in
+  let fold e el = intern_rec_with_constraint env e t0 :: el in
   let el = e0 :: List.fold_right fold el [] in
   (GTacArr el, GTypRef (t_array, [t0]))
 | CTacLst (loc, []) ->
@@ -584,12 +611,7 @@ let rec intern_rec env = function
   (c_nil, GTypRef (t_list, [GTypVar id]))
 | CTacLst (loc, e0 :: el) ->
   let (e0, t0) = intern_rec env e0 in
-  let fold e el =
-    let loc = loc_of_tacexpr e in
-    let (e, t) = intern_rec env e in
-    let () = unify loc env t t0 in
-    c_cons e el
-  in
+  let fold e el = c_cons (intern_rec_with_constraint env e t0) el in
   let el = c_cons e0 (List.fold_right fold el c_nil) in
   (el, GTypRef (t_list, [t0]))
 | CTacCnv (loc, e, tc) ->
@@ -604,6 +626,34 @@ let rec intern_rec env = function
   (GTacLet (false, [Anonymous, e1], e2), t2)
 | CTacCse (loc, e, pl) ->
   intern_case env loc e pl
+| CTacRec (loc, fs) ->
+  intern_record env loc fs
+| CTacPrj (loc, e, proj) ->
+  let pinfo = get_projection proj in
+  let loc = loc_of_tacexpr e in
+  let (e, t) = intern_rec env e in
+  let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
+  let params = Array.map_to_list (fun i -> GTypVar i) subst in
+  let exp = GTypRef (pinfo.pdata_type, params) in
+  let () = unify loc env t exp in
+  let substf i = GTypVar subst.(i) in
+  let ret = subst_type substf pinfo.pdata_ptyp in
+  (GTacPrj (e, pinfo.pdata_indx), ret)
+| CTacSet (loc, e, proj, r) ->
+  let pinfo = get_projection proj in
+  let () =
+    if not pinfo.pdata_mutb then
+      let (loc, _) = proj in
+      user_err ~loc (str "Field is not mutable")
+  in
+  let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
+  let params = Array.map_to_list (fun i -> GTypVar i) subst in
+  let exp = GTypRef (pinfo.pdata_type, params) in
+  let e = intern_rec_with_constraint env e exp in
+  let substf i = GTypVar subst.(i) in
+  let ret = subst_type substf pinfo.pdata_ptyp in
+  let r = intern_rec_with_constraint env r ret in
+  (GTacSet (e, pinfo.pdata_indx, r), GTypRef (t_unit, []))
 | CTacExt (loc, ext) ->
   let open Genintern in
   let GenArg (Rawwit tag, _) = ext in
@@ -616,6 +666,12 @@ let rec intern_rec env = function
   let (_, ext) = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> generic_intern ist ext) () in
   (GTacExt ext, GTypRef (tpe.ml_type, []))
 
+and intern_rec_with_constraint env e exp =
+  let loc = loc_of_tacexpr e in
+  let (e, t) = intern_rec env e in
+  let () = unify loc env t exp in
+  e
+
 and intern_let_rec env loc el e =
   let fold accu ((loc, na), _, _) = match na with
   | Anonymous -> accu
@@ -760,12 +816,9 @@ and intern_case env loc e pl =
         in
         let ids = List.map get_id args in
         let nids = List.length ids in
-        let nargs = List.length (snd data.cdata_args) in
+        let nargs = List.length data.cdata_args in
         let () =
-          if not (Int.equal nids nargs) then
-            user_err ~loc (str "Constructor expects " ++ int nargs ++
-              str " arguments, but is applied to " ++ int nids ++
-              str " arguments")
+          if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids
         in
         let fold env id tpe =
           (** Instantiate all arguments *)
@@ -773,7 +826,7 @@ and intern_case env loc e pl =
           let tpe = subst_type subst tpe in
           push_name id (monomorphic tpe) env
         in
-        let nenv = List.fold_left2 fold env ids (snd data.cdata_args) in
+        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
@@ -802,6 +855,64 @@ and intern_case env loc e pl =
     let ce = GTacCse (e', GCaseAlg kn, const, nonconst) in
     (ce, ret)
 
+and intern_constructor env loc kn args =
+  let cstr = interp_constructor kn in
+  let nargs = List.length cstr.cdata_args in
+  if Int.equal nargs (List.length args) then
+    let subst = Array.init cstr.cdata_prms (fun _ -> fresh_id env) in
+    let substf i = GTypVar subst.(i) in
+    let types = List.map (fun t -> subst_type substf t) cstr.cdata_args in
+    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 (cstr.cdata_type, cstr.cdata_indx, args), ans)
+  else
+    error_nargs_mismatch loc nargs (List.length args)
+
+and intern_record env loc fs =
+  let map ((loc, qid), e) =
+    let proj = get_projection (loc, qid) in
+    (loc, proj, e)
+  in
+  let fs = List.map map fs in
+  let kn = match fs with
+  | [] -> user_err ~loc (str "Cannot infer the corresponding record type")
+  | (_, proj, _) :: _ -> proj.pdata_type
+  in
+  let params, typdef = match Tac2env.interp_type kn with
+  | n, GTydRec def -> n, def
+  | _ -> assert false
+  in
+  let subst = Array.init params (fun _ -> fresh_id env) in
+  (** Set the answer [args] imperatively *)
+  let args = Array.make (List.length typdef) None in
+  let iter (loc, pinfo, e) =
+    if KerName.equal kn pinfo.pdata_type then
+      let index = pinfo.pdata_indx in
+      match args.(index) with
+      | None ->
+        let exp = subst_type (fun i -> GTypVar subst.(i)) pinfo.pdata_ptyp in
+        let e = intern_rec_with_constraint env e exp in
+        args.(index) <- Some e
+      | Some _ ->
+        let (name, _, _) = List.nth typdef pinfo.pdata_indx in
+        user_err ~loc (str "Field " ++ Id.print name ++ str " is defined \
+          several times")
+    else
+      user_err ~loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
+        pertain to record definition " ++ KerName.print pinfo.pdata_type)
+  in
+  let () = List.iter iter fs in
+  let () = match Array.findi (fun _ o -> Option.is_empty o) args with
+  | None -> ()
+  | Some i ->
+    let (field, _, _) = List.nth typdef i in
+    user_err ~loc (str "Field " ++ Id.print field ++ str " is undefined")
+  in
+  let args = Array.map_to_list Option.get args in
+  let tparam = List.init params (fun i -> GTypVar subst.(i)) in
+  (GTacCst (kn, 0, args), GTypRef (kn, tparam))
+
 let normalize env (count, vars) (t : UF.elt glb_typexpr) =
   let get_var id =
     try UF.Map.find id !vars
@@ -907,6 +1018,13 @@ 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')
+| GTacPrj (e, p) as e0 ->
+  let e' = subst_expr subst e in
+  if e' == e then e0 else GTacPrj (e', p)
+| GTacSet (e, p, r) as e0 ->
+  let e' = subst_expr subst e in
+  let r' = subst_expr subst r in
+  if e' == e && r' == r then e0 else GTacSet (e', p, r')
 | GTacExt ext ->
   let ext' = Genintern.generic_substitute subst ext in
   if ext' == ext then e else GTacExt ext'
diff --git a/tac2interp.ml b/tac2interp.ml
index b868caf963..fedbb13e7d 100644
--- a/tac2interp.ml
+++ b/tac2interp.ml
@@ -80,6 +80,12 @@ 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
+| 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
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   Tac2env.interp_primitive ml el
@@ -110,3 +116,16 @@ and interp_case ist e cse0 cse1 = match e with
   interp ist e
 | 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 _ ->
+  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 _ ->
+  anomaly (str "Unexpected value shape")