aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--pretyping/patternops.ml49
-rw-r--r--pretyping/patternops.mli3
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/tacinterp.ml10
5 files changed, 42 insertions, 30 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28d5..2a2ef30fb1 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
let i = destRel (Array.last args) in
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
- PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+ PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
| Cast (c,_,_) -> aux c
- | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+ | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
in
aux bodyi
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9aec..009b7323e4 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
let pattern_of_constr env sigma t =
let ctx = ref [] in
+ let keep = ref Evar.Set.empty in
+ let remove = ref Evar.Set.empty in
let rec pattern_of_constr env t =
match kind_of_term t with
| Rel n -> PRel n
@@ -141,28 +143,35 @@ let pattern_of_constr env sigma t =
| App (f,a) ->
(match
match kind_of_term f with
- Evar (evk,args as ev) ->
- (match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (true,id) ->
- ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
- Some id
- | _ -> None)
- | _ -> None
- with
- | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
- | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+ | Evar (evk,args as ev) ->
+ (match snd (Evd.evar_source evk sigma) with
+ Evar_kinds.MatchingVar (true,id) ->
+ let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ ctx := (id,None,ty)::!ctx;
+ keep := Evar.Set.union (evars_of_term ty) !keep;
+ remove := Evar.Set.add evk !remove;
+ Some id
+ | _ -> None)
+ | _ -> None
+ with
+ | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+ | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
| Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
| Ind (sp,u) -> PRef (canonical_gr (IndRef sp))
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
| Proj (p, c) ->
pattern_of_constr env (Retyping.expand_projection env sigma p c [])
| Evar (evk,ctxt as ev) ->
- (match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (b,id) ->
- ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
- assert (not b); PMeta (Some id)
- | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
- | _ -> PMeta None)
+ remove := Evar.Set.add evk !remove;
+ (match snd (Evd.evar_source evk sigma) with
+ | Evar_kinds.MatchingVar (b,id) ->
+ let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ ctx := (id,None,ty)::!ctx;
+ keep := Evar.Set.union (evars_of_term ty) !keep;
+ assert (not b); PMeta (Some id)
+ | Evar_kinds.GoalEvar ->
+ PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+ | _ -> PMeta None)
| Case (ci,p,a,br) ->
let cip =
{ cip_style = ci.ci_pp_info.style;
@@ -178,9 +187,11 @@ let pattern_of_constr env sigma t =
| Fix f -> PFix f
| CoFix f -> PCoFix f in
let p = pattern_of_constr env t in
+ let remove = Evar.Set.diff !remove !keep in
+ let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
(* side-effect *)
(* Warning: the order of dependencies in ctx is not ensured *)
- (!ctx,p)
+ (sigma,!ctx,p)
(* To process patterns, we need a translation without typing at all. *)
@@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c =
ctx
in
let c = substl inst c in
- snd (pattern_of_constr env sigma c)
+ pi3 (pattern_of_constr env sigma c)
with Not_found (* List.index failed *) ->
let vars =
List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +256,7 @@ let rec subst_pattern subst pat =
| PRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then pat else
- snd (pattern_of_constr (Global.env()) Evd.empty t)
+ pi3 (pattern_of_constr (Global.env()) Evd.empty t)
| PVar _
| PEvar _
| PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c24..9e72280fe2 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
existential variable are allowed in [c] *)
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr ->
+ Evd.evar_map * named_context * constr_pattern
(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5621c365aa..101223b570 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -609,7 +609,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
match kind_of_term cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = snd (Patternops.pattern_of_constr env sigma cty) in
+ let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -628,7 +628,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = snd (Patternops.pattern_of_constr env ce.evd c') in
+ let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
@@ -726,7 +726,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd, { pri=1;
poly = poly;
- pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+ pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
name = name;
code=Res_pf_THEN_trivial_fail(c,t,ctx) })
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8826875a38..1429211f19 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -681,7 +681,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
let p = match a with
| Inl b -> Inl (interp_evaluable ist env sigma b)
- | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
+ | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
interp_occurrences ist occs, p
let interp_constr_with_occurrences_and_name_as_list =
@@ -1030,7 +1030,7 @@ let use_types = false
let eval_pattern lfun ist env sigma (_,pat as c) =
if use_types then
- snd (interp_typed_pattern ist env sigma c)
+ pi3 (interp_typed_pattern ist env sigma c)
else
instantiate_pattern env sigma lfun pat
@@ -2138,7 +2138,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
Proofview.V82.tactic begin fun gl ->
- let sign,op = interp_typed_pattern ist env sigma op in
+ let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
let env' = Environ.push_named_context sign env in
let c_interp sigma =
@@ -2146,8 +2146,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
with e when to_catch e (* Hack *) ->
errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
- (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
- gl
+ (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
+ { gl with sigma = sigma }
end
end
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 19:52:20 +0000