diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index d996443d61..b5b8697d25 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -173,11 +173,12 @@ let interp_recursive ~program_mode ~cofix fixl notations = | None , acc -> acc | x , None -> x | Some ls , Some us -> - let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + let open UState in + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in + let sigma, decl = interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in @@ -253,7 +254,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) + Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) |