diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 8 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 8 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 16 |
3 files changed, 24 insertions, 8 deletions
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 |