diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index b95741ca..ad21a6d9 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -44,7 +44,7 @@ let mkSubset sigma name typ prop = let sigT = Lazy.from_fun build_sigma_type -let make_qref s = CAst.make @@ Qualid (qualid_of_string s) +let make_qref s = qualid_of_string s let lt_ref = make_qref "Init.Peano.lt" let rec telescope sigma l = @@ -91,7 +91,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let sigma, decl = Univdecls.interp_univ_decl_opt env pl in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in @@ -187,12 +187,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, def = let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in let sigma, h_e_term = Evarutil.new_evar env sigma - ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in + ~src:(Loc.tag @@ Evar_kinds.QuestionMark { + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false; + }) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in - let _evd = ref sigma in - let def = Typing.e_solve_evars env _evd def in - let sigma = !_evd in + let sigma, def = Typing.solve_evars env sigma def in let sigma = Evarutil.nf_evar_map sigma in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context sigma binders_rel in @@ -214,7 +214,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in - let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in + let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in @@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - let fullcoqc = EConstr.to_constr sigma def in + (* XXX: Grounding non-ground terms here... bad bad *) + let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = @@ -254,16 +255,17 @@ let do_program_recursive local poly fixkind fixl ntns = interp_recursive ~cofix ~program_mode:true fixl ntns in (* Program-specific code *) - (* Get the interesting evars, those that were not instanciated *) + (* Get the interesting evars, those that were not instantiated *) let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in (* Solve remaining evars *) let evd = nf_evar_map_undefined evd in let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) and typ = - EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) + (* Worrying... *) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = |