diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:52:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-28 18:58:06 +0100 |
| commit | 7b724139a09c5d875131c5861a32d225d5b4b07b (patch) | |
| tree | 3f556cc57d2b9500ecd972f97b2a25824c491dbe /interp | |
| parent | 8b42c73a6a3b417e848952e7510e27d74e6e1758 (diff) | |
Constructor type information uses the expanded form.
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/impargs.ml | 5 |
2 files changed, 6 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 24894fc9f5..7f1dc70d95 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1188,7 +1188,6 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) -open Term open Declarations (* Similar to Cases.adjust_local_defs but on RCPat *) @@ -1197,16 +1196,15 @@ let insert_local_defs_in_pattern (ind,j) 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 (Context.Rel.length mib.mind_params_ctxt) typi in - let (decls,_) = decompose_prod_assum typi in + let (ctx, _) = mip.mind_nf_lc.(j-1) in + let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in let rec aux decls args = match decls, args with | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) l + aux decls l let add_local_defs_and_check_length loc env g pl args = match g with | ConstructRef cstr -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 6fd52d98dd..2c281af2d2 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -452,9 +452,10 @@ let compute_mib_implicits flags kn = let ind = (kn,i) in let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), - Array.mapi (fun j c -> + Array.mapi (fun j (ctx, cty) -> + let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) - (Array.map of_constr mip.mind_nf_lc)) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets |