diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index aa2362ae5..367425546 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -38,6 +38,7 @@ open Ind_tables open Auto_ind_decl open Eqschemes open Elimschemes +open Context.Rel.Declaration (* Flags governing automatic synthesis of schemes *) @@ -470,7 +471,7 @@ let build_combined_scheme env schemes = in let ctx, _ = list_split_rev_at prods - (List.rev_map (fun (x, y) -> x, None, y) ctx) in + (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = it_mkProd_wo_LetIn concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in (body, typ) |