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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/formula.ml | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 3 |
3 files changed, 7 insertions, 6 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 204f889f90..ef6c07bff2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1044,7 +1044,9 @@ let fake_match_projection env p = let indu = mkIndU (ind,u) in let ctx, paramslet = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + let (ctx, cty) = mip.mind_nf_lc.(0) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in List.chop mip.mind_consnrealdecls.(0) rctx in let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index a60a966cec..56b3dc97cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -13,7 +13,6 @@ open Names open Constr open EConstr open Vars -open Termops open Util open Declarations open Globnames @@ -100,9 +99,8 @@ let kind_of_formula env sigma term = else let has_realargs=(n>0) in let is_trivial= - let is_constant c = - Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - Array.exists is_constant mip.mind_nf_lc in + let is_constant n = Int.equal n 0 in + Array.exists is_constant mip.mind_consnrealargs in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..7216849948 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in |