Ltac2: support pure projections as syntactic values

plugins/ltac2/tac2intern.ml

@@ -115,6 +115,13 @@ let is_pure_constructor kn =
     List.for_all is_pure fields
   | GTydDef _ -> assert false (** Type definitions have no constructors *)
 
+let is_pure_field kn i =
+  match snd (Tac2env.interp_type kn) with
+  | GTydRec fields ->
+    let is_pure (_, mut, _) = not mut in
+    is_pure (List.nth fields i)
+  | GTydAlg _ | GTydOpn | GTydDef _ -> assert false
+
 let rec is_value = function
 | GTacAtm (AtmInt _) | GTacVar _ | GTacPrm _ -> true
 | GTacFun (bnd,_) -> assert (not (CList.is_empty bnd)); true
@@ -127,7 +134,8 @@ let rec is_value = function
 | GTacLet (_, bnd, e) ->
   (* in the recursive case the bnd are guaranteed to be values but it doesn't hurt to check *)
   is_value e && List.for_all (fun (_, e) -> is_value e) bnd
-| GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _
+| GTacPrj (kn,e,i) -> is_pure_field kn i && is_value e
+| GTacCse _ | GTacSet _ | GTacExt _
 | GTacWth _ | GTacFullMatch _ -> false
 
 let is_rec_rhs = function

plugins/ltac2/tac2interp.ml

@@ -258,11 +258,14 @@ and eval_pure bnd kn = function
 | GTacLet (true, el, body) ->
   let bnd = push_let_rec bnd el in
   eval_pure bnd kn body
+| GTacPrj (_,e,i) ->
+  let v = eval_pure bnd kn e in
+  Valexpr.field v i
 
 | GTacPrm ml -> Tac2env.interp_primitive ml
 
 | GTacAtm (AtmStr _) | GTacSet _
-| GTacApp _ | GTacCse _ | GTacPrj _
+| GTacApp _ | GTacCse _
 | GTacExt _ | GTacWth _
 | GTacFullMatch _ ->
   anomaly (Pp.str "Term is not a syntactical value")