Better support for printing constructors with let-ins.

This allows e.g. to use the record notations even when there are
defined fields.

A priori fixed also missing parameters when interpreting primitive
tokens.

1 files changed, 33 insertions, 0 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 51660818f..0eda77651 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function
       PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
   | _ -> raise Not_found
 
+open Declarations
+open Term
+open Context
+
+(* Keep only patterns which are not bound to a local definitions *)
+let drop_local_defs typi args =
+    let (decls,_) = decompose_prod_assum typi in
+    let rec aux decls args =
+      match decls, args with
+      | [], [] -> []
+      | Rel.Declaration.LocalDef _ :: decls, pat :: args ->
+         begin
+           match pat with
+           | PatVar (_,Anonymous) -> aux decls args
+           | _ -> raise Not_found (* The pattern is used, one cannot drop it *)
+         end
+      | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+      | _ -> assert false in
+    aux (List.rev decls) args
+
+let add_patterns_for_params_remove_local_defs (ind,j) l =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let nparams = mib.Declarations.mind_nparams in
+  let l =
+    if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+      (* Optimisation *) l
+    else
+      let typi = mip.mind_nf_lc.(j-1) in
+      let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
+      drop_local_defs typi l in
+  Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
+
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_closed_cases_pattern_aux = function
   | PatCstr (loc,cstr,[],Anonymous) ->
       GRef (loc,ConstructRef cstr,None)
   | PatCstr (loc,cstr,l,Anonymous) ->
       let ref = GRef (loc,ConstructRef cstr,None) in
+      let l = add_patterns_for_params_remove_local_defs cstr l in
       GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found