diff options
| author | Gaëtan Gilbert | 2019-03-06 20:58:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-06 20:58:26 +0100 |
| commit | c9fd99644e223ada3aad53915f1cd0d2598882b3 (patch) | |
| tree | 784938d42cf4c37436c305cf625d240c154ac9c9 /plugins/ssr | |
| parent | a83eac8463787c13a2dbd3903baf2b59ca1a4635 (diff) | |
| parent | 7b724139a09c5d875131c5861a32d225d5b4b07b (diff) | |
Merge PR #9476: Constructor type information uses the expanded form.
Reviewed-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |