diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/himsg.ml | 8 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/proof_using.ml | 10 |
4 files changed, 11 insertions, 13 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index eef7afbfba..102a98f046 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -187,7 +187,9 @@ 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 sigma, def = Typing.solve_evars env sigma def in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 534e58f9c9..c49ffe2679 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -520,11 +520,15 @@ let pr_trailing_ne_context_of env sigma = then str "." else (str " in environment:"++ pr_context_unlimited env sigma) -let rec explain_evar_kind env sigma evk ty = function +let rec explain_evar_kind env sigma evk ty = + let open Evar_kinds in + function | Evar_kinds.NamedHole id -> strbrk "the existential variable named " ++ Id.print id - | Evar_kinds.QuestionMark _ -> + | Evar_kinds.QuestionMark {qm_record_field=None} -> strbrk "this placeholder of type " ++ ty + | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} -> + str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname) | Evar_kinds.CasesType false -> strbrk "the type of this pattern-matching problem" | Evar_kinds.CasesType true -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1f401b4e15..14d7642328 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty = in let loc, k = evar_source id evm in let status = match k with - | Evar_kinds.QuestionMark (o,_) -> o + | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with | Some o -> o | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 74e53bef18..3e2bd98720 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration let known_names = Summary.ref [] ~name:"proofusing-nameset" -let in_nameset = - let open Libobject in - declare_object { (default_object "proofusing-nameset") with - cache_function = (fun (_,x) -> known_names := x :: !known_names); - classify_function = (fun _ -> Dispose); - discharge_function = (fun _ -> None) - } - let rec close_fwd e s = let s' = List.fold_left (fun s decl -> @@ -73,7 +65,7 @@ let process_expr env e ty = let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s -let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) +let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = let rec aux ids = |