aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml4
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/proofview.ml6
-rw-r--r--engine/termops.ml1
-rw-r--r--interp/constrintern.ml12
-rw-r--r--intf/evar_kinds.mli2
-rw-r--r--plugins/ltac/extratactics.ml46
-rw-r--r--pretyping/cases.ml8
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/pretyping.ml16
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--test-suite/.csdp.cachebin89077 -> 89077 bytes
-rw-r--r--test-suite/output/Show.out6
-rw-r--r--test-suite/output/inference.out10
-rw-r--r--test-suite/output/inference.v2
-rw-r--r--test-suite/output/names.out6
-rw-r--r--test-suite/output/names.v4
-rw-r--r--test-suite/success/Abstract.v1
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/obligations.ml2
22 files changed, 69 insertions, 36 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6cba6f607..3ef725cbb 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
let evd = Sigma.to_evar_map evd in
let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
- let evd, evk' = Evd.restrict evk filter ?candidates evd in
+ let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
let new_pure_evar_full evd evi =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index fcc435a2e..496ec5bc4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
- constr list option -> (existential_key, 'r) Sigma.sigma
+ ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
(** Polymorphic constants *)
diff --git a/engine/evd.ml b/engine/evd.ml
index b677705bc..48fceae9e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -653,12 +653,13 @@ let define evk body evd =
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
{ evd with defn_evars; undf_evars; last_mods; evar_names }
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
let evar_info' =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
evar_extra = Store.empty } in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
diff --git a/engine/evd.mli b/engine/evd.mli
index 005332470..86755c360 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
(** {6 Misc} *)
val restrict : evar -> Filter.t -> ?candidates:constr list ->
- evar_map -> evar_map * evar
+ ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
(** Restrict an undefined evar into a new evar by filtering context and
possibly limiting the instances to a set of candidates *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ddfc0e39d..29bb1ef39 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
let info =
if goal then
{ info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
| _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
| loc,_ -> loc,Evar_kinds.GoalEvar }
else info
diff --git a/engine/termops.ml b/engine/termops.ml
index ca32c06a7..1ec2b8103 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -112,6 +112,7 @@ let pr_evar_suggested_name evk sigma =
| None -> match evi.evar_source with
| _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
| _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.QuestionMark (_,Name id) -> id
| _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
| _ ->
let env = reset_with_named_context evi.evar_hyps (Global.env()) in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287ef..6514ad8be 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer =
let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
match projs with
| [] -> (idx, acc_first_idx, acc)
- | (Some name) :: projs ->
- let field_glob_ref = ConstRef name in
+ | (Some field_glob_id) :: projs ->
+ let field_glob_ref = ConstRef field_glob_id in
let first_field = eq_gr field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch")
@@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer =
build_proj_list projs proj_kinds idx ~acc_first_idx acc
else
build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
- ((idx, field_glob_ref) :: acc)
+ ((idx, field_glob_id) :: acc)
end
| None :: projs ->
if complete then
@@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer =
user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+ let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
@@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
sort_fields ~complete:true loc fs
- (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+ (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
Misctypes.IntroAnonymous, None))
in
begin
@@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
(match naming with
| Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
- | _ -> Evar_kinds.QuestionMark st)
+ | _ -> Evar_kinds.QuestionMark (st,Anonymous))
| Some k -> k
in
let solve = match solve with
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 470ad2a23..835e94c77 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -21,7 +21,7 @@ type t =
* bool (** Force inference *)
| BinderType of Name.t
| NamedHole of Id.t (* coming from some ?[id] syntax *)
- | QuestionMark of obligation_definition_status
+ | QuestionMark of obligation_definition_status * Name.t
| CasesType of bool (* true = a subterm of the type *)
| InternalHole
| TomatchTypeParameter of inductive * int
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b..cba9c1364 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t =
else
(incr locref;
CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
+ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
Misctypes.IntroAnonymous, None)))
else x
| c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
let locref = ref 0 in
let occref = ref occ in
let rec substrec = function
- | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
+ | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
| c -> map_glob_constr_left_to_right substrec c
in
substrec t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a9..426157372 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y =
let mk_JMeq_refl evdref typ x =
papp evdref coq_JMeq_refl [| typ; x |]
-let hole = CAst.make @@
- GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
Misctypes.IntroAnonymous, None)
let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx =
prev,
(CAst.make @@ GApp (
(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)),
- [hole; CAst.make @@ GVar prev])) :: vars
+ [hole na; CAst.make @@ GVar prev])) :: vars
| _ ->
match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
@@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
| l -> CAst.make @@ GApp (bref, l)
in
let branch = match ineqs with
- Some _ -> CAst.make @@ GApp (branch, [ hole ])
+ Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
| None -> branch
in
incr i;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3ef17912f..83c26058a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
open Program
-let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c =
- let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
+let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
+ let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
Evarutil.e_new_evar env evdref ~src c
let app_opt env evdref f t =
@@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
- let evar = make_existential ?loc env evdref eq in
+ let evar = make_existential ?loc n env evdref eq in
let eq_app x = papp evdref coq_eq_rect
[| eqT; hdx; pred; x; hdy; evar|]
in
@@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
Some
(fun x ->
let cx = app_opt env evdref c x in
- let evar = make_existential ?loc env evdref (mkApp (p, [| cx |]))
+ let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
in
(papp evdref sig_intro [| u; p; cx; evar |]))
| None ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e72394fa2..b0663af70 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c
+let adjust_evar_source evdref na c =
+ match na, kind !evdref c with
+ | Name id, Evar (evk,args) ->
+ let evi = Evd.find !evdref evk in
+ begin match evi.evar_source with
+ | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
+ let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+ let sigma = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
+ evdref := Sigma.to_evar_map evd;
+ mkEvar (evk',args)
+ | _ -> c
+ end
+ | _, _ -> c
+
(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref false
@@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
args, nf_evar !evdref (j_val hj)
else [], j_val hj
in
+ let ujval = adjust_evar_source evdref na ujval in
let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
let j = { uj_val = value; uj_type = typ } in
apply_rec env (n+1) j candargs rest
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe64..35fbec5a6 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -254,7 +254,7 @@ open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
let mkGApp f args = CAst.make @@ GApp (f, args)
let mkGHole = CAst.make @@
- GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None)
+ GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
let mkGProd id c1 c2 = CAst.make @@
GProd (Name (Id.of_string id), Explicit, c1, c2)
let mkGArrow c1 c2 = CAst.make @@
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95..ba85286dd 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809..8acfed5d0 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,12 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
H : 0 = 0
============================
1 = 1
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
S (S n') = S m
(dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912..d28ee4276 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
: option L -> option L
fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
: forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
: forall n : nat, T n
where
-?t : [n : nat x := A n : T n |- ?T -> T n]
-?y : [n : nat x := A n : T n |- ?T]
-fun n : nat => ?t ?y : T n
+?t : [n : nat y := A n : T n |- ?T -> T n]
+?x : [n : nat y := A n : T n |- ?T]
+fun n : nat => ?t ?x : T n
: forall n : nat, T n
where
?t : [n : nat |- ?T -> T n]
-?y : [n : nat |- ?T]
+?x : [n : nat |- ?T]
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db167..f761a4dc5 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
(* Note: exact numbers of evars are not important... *)
Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892d..48be63a46 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
y : nat
The term "a y" has type "{y0 : nat | y = y0}"
while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+
+ H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+ ============================
+ True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a0..f1efd0df2 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
Parameter a : forall x, {y:nat|x=y}.
Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6ef..69dc9aca7 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
(* Cf coqbugs #546 *)
Require Import Omega.
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7f..25dd724af 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1062,7 +1062,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar env evdref
- ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+ ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
prop |])
in
let def = Typing.e_solve_evars env evdref def in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index be58c67a9..47ac16f9c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -221,7 +221,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 (o,_) -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 09:35:02 +0000