aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/quote/quote.ml2
-rw-r--r--pretyping/constrMatching.ml82
-rw-r--r--pretyping/constrMatching.mli20
-rw-r--r--pretyping/evarconv.ml39
-rw-r--r--pretyping/evarsolve.ml23
-rw-r--r--pretyping/evarsolve.mli4
-rw-r--r--pretyping/tacred.ml9
-rw-r--r--tactics/auto.ml15
-rw-r--r--tactics/hipattern.ml43
-rw-r--r--tactics/tacticMatching.ml4
-rw-r--r--test-suite/bugs/closed/3377.v (renamed from test-suite/bugs/opened/3377.v)10
-rw-r--r--toplevel/search.ml11
12 files changed, 135 insertions, 87 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ea459e551f..7ed4a0dbcd 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -401,7 +401,7 @@ let quote_terms ivs lc =
match l with
| (lhs, rhs)::tail ->
begin try
- let s1 = Id.Map.bindings (matches rhs c) in
+ let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs c) in
let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
in
Termops.subst_meta s2 lhs
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 423ce4cb12..e4b6144082 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -138,18 +138,18 @@ let merge_binding allow_bound_rels stk n cT subst =
in
constrain n c subst
-let matches_core convert allow_partial_app allow_bound_rels pat c =
+let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
let convref ref c =
match ref, kind_of_term c with
| VarRef id, Var id' -> Names.id_eq id id'
| ConstRef c, Const (c',_) -> Names.eq_constant c c'
| IndRef i, Ind (i', _) -> Names.eq_ind i i'
| ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
- | _, _ -> (match convert with
- | None -> false
- | Some (env,sigma) ->
- let sigma,c' = Evd.fresh_global env sigma ref in
- is_conv env sigma c' c)
+ | _, _ ->
+ (if convert then
+ let sigma,c' = Evd.fresh_global env sigma ref in
+ is_conv env sigma c' c
+ else false)
in
let rec sorec stk subst p t =
let cT = strip_outer_cast t in
@@ -211,6 +211,12 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
(try Array.fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure))
+ | PApp (PMeta (Some n), [|c1|]), Proj (p2, c2) ->
+ let ty = Retyping.get_type_of env sigma c2 in
+ let term = mkLambda (Name (id_of_string "x"), ty, mkProj (p2, mkRel 1)) in
+ let subst = merge_binding allow_bound_rels stk n term subst in
+ sorec stk subst c1 c2
+
| PApp (PRef (ConstRef c1),arg1), Proj (p2,c2) when eq_constant c1 p2 ->
let pb = Environ.lookup_projection p2 (Global.env ()) in
let pars = pb.Declarations.proj_npars in
@@ -277,13 +283,13 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
in
sorec [] (Id.Map.empty, Id.Map.empty) pat c
-let matches_core_closed convert allow_partial_app pat c =
- let names, subst = matches_core convert allow_partial_app false pat c in
+let matches_core_closed env sigma convert allow_partial_app pat c =
+ let names, subst = matches_core env sigma convert allow_partial_app false pat c in
(names, Id.Map.map snd subst)
-let extended_matches = matches_core None true true
+let extended_matches env sigma = matches_core env sigma false true true
-let matches pat c = snd (matches_core_closed None true pat c)
+let matches env sigma pat c = snd (matches_core_closed env sigma false true pat c)
let special_meta = (-1)
@@ -295,7 +301,7 @@ let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
let isPMeta = function PMeta _ -> true | _ -> false
-let matches_head pat c =
+let matches_head env sigma pat c =
let head =
match pat, kind_of_term c with
| PApp (c1,arg1), App (c2,arg2) ->
@@ -304,40 +310,40 @@ let matches_head pat c =
if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c
| c1, App (c2,arg2) when not (isPMeta c1) -> c2
| _ -> c in
- matches pat head
+ matches env sigma pat head
(* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ partial_app closed pat c mk_ctx next =
+let authorized_occ env sigma partial_app closed pat c mk_ctx next =
try
- let sigma = matches_core_closed None partial_app pat c in
- if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma)
+ let subst = matches_core_closed env sigma false partial_app pat c in
+ if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst)
then next ()
- else mkresult sigma (mk_ctx (mkMeta special_meta)) next
+ else mkresult subst (mk_ctx (mkMeta special_meta)) next
with PatternMatchingFailure -> next ()
(* Tries to match a subterm of [c] with [pat] *)
-let sub_match ?(partial_app=false) ?(closed=true) pat c =
+let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let rec aux c mk_ctx next =
match kind_of_term c with
| Cast (c1,k,c2) ->
let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
let next () = try_aux [c1] next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Lambda (x,c1,c2) ->
let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
let next () = try_aux [c1;c2] next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Prod (x,c1,c2) ->
let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
let next () = try_aux [c1;c2] next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| LetIn (x,c1,t,c2) ->
let next_mk_ctx = function
| [c1;c2] -> mkLetIn (x,c1,t,c2)
| _ -> assert false
in
let next () = try_aux [c1;c2] next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| App (c1,lc) ->
let next () =
let topdown = true in
@@ -367,14 +373,14 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
try_aux (c1::Array.to_list lc) mk_ctx next
in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Case (ci,hd,c1,lc) ->
let next_mk_ctx = function
| [] -> assert false
| c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
in
let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Fix (indx,(names,types,bodies)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
@@ -383,7 +389,7 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
let next () =
try_aux
((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| CoFix (i,(names,types,bodies)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
@@ -391,13 +397,13 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
let next () =
try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Proj (p,c') ->
let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
let next () = try_aux [c'] next_mk_ctx next in
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
| Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
- authorized_occ partial_app closed pat c mk_ctx next
+ authorized_occ env sigma partial_app closed pat c mk_ctx next
(* Tries [sub_match] for all terms in the list *)
and try_aux lc mk_ctx next =
@@ -412,26 +418,28 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
let result () = aux c (fun x -> x) lempty in
IStream.thunk result
-let match_subterm pat c = sub_match pat c
+let match_subterm env sigma pat c = sub_match env sigma pat c
-let match_appsubterm pat c = sub_match ~partial_app:true pat c
+let match_appsubterm env sigma pat c =
+ sub_match ~partial_app:true env sigma pat c
-let match_subterm_gen app pat c = sub_match ~partial_app:app pat c
+let match_subterm_gen env sigma app pat c =
+ sub_match ~partial_app:app env sigma pat c
-let is_matching pat c =
- try let _ = matches pat c in true
+let is_matching env sigma pat c =
+ try let _ = matches env sigma pat c in true
with PatternMatchingFailure -> false
-let is_matching_head pat c =
- try let _ = matches_head pat c in true
+let is_matching_head env sigma pat c =
+ try let _ = matches_head env sigma pat c in true
with PatternMatchingFailure -> false
-let is_matching_appsubterm ?(closed=true) pat c =
- let results = sub_match ~partial_app:true ~closed pat c in
+let is_matching_appsubterm ?(closed=true) env sigma pat c =
+ let results = sub_match ~partial_app:true ~closed env sigma pat c in
not (IStream.is_empty results)
let matches_conv env sigma c p =
- snd (matches_core_closed (Some (env,sigma)) false c p)
+ snd (matches_core_closed env sigma true false c p)
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/constrMatching.mli b/pretyping/constrMatching.mli
index 19cf348775..a4e797dae0 100644
--- a/pretyping/constrMatching.mli
+++ b/pretyping/constrMatching.mli
@@ -30,31 +30,31 @@ type bound_ident_map = Id.t Id.Map.t
assignment of metavariables; it raises [PatternMatchingFailure] if
not matchable; bindings are given in increasing order based on the
numbers given in the pattern *)
-val matches : constr_pattern -> constr -> patvar_map
+val matches : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
(** [matches_head pat c] does the same as [matches pat c] but accepts
[pat] to match an applicative prefix of [c] *)
-val matches_head : constr_pattern -> constr -> patvar_map
+val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
(** [extended_matches pat c] also returns the names of bound variables
in [c] that matches the bound variables in [pat]; if several bound
variables or metavariables have the same name, the metavariable,
or else the rightmost bound variable, takes precedence *)
val extended_matches :
- constr_pattern -> constr -> bound_ident_map * extended_patvar_map
+ env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map
(** [is_matching pat c] just tells if [c] matches against [pat] *)
-val is_matching : constr_pattern -> constr -> bool
+val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
(** [is_matching_head pat c] just tells if [c] or an applicative
prefix of it matches against [pat] *)
-val is_matching_head : constr_pattern -> constr -> bool
+val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool
(** [matches_conv env sigma] matches up to conversion in environment
[(env,sigma)] when constants in pattern are concerned; it raises
[PatternMatchingFailure] if not matchable; bindings are given in
increasing order based on the numbers given in the pattern *)
-val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
+val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
(** The type of subterm matching results: a substitution + a context
(whose hole is denoted here with [special_meta]) *)
@@ -64,20 +64,20 @@ type matching_result =
(** [match_subterm n pat c] returns the substitution and the context
corresponding to each **closed** subterm of [c] matching [pat]. *)
-val match_subterm : constr_pattern -> constr -> matching_result IStream.t
+val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
(** [match_appsubterm pat c] returns the substitution and the context
corresponding to each **closed** subterm of [c] matching [pat],
considering application contexts as well. *)
-val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t
+val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : bool (** true = with app context *) ->
+val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) ->
constr_pattern -> constr -> matching_result IStream.t
(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
against [pat] taking partial subterms into consideration *)
-val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool
+val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool
(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
up to conversion for constants in patterns *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 68dfb1a1bd..1a699f4afb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -319,17 +319,22 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
destroy beta-redexes that can be used for 1st-order unification *)
let term1 = apprec_nohdbeta ts env evd term1 in
let term2 = apprec_nohdbeta ts env evd term2 in
+ let default () = evar_eqappr_x ts env evd pbty
+ (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
+ (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+ in
begin match kind_of_term term1, kind_of_term term2 with
| Evar ev, _ when Evd.is_undefined evd (fst ev) ->
- solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem true pbty,ev,term2)
+ (match solve_simple_eqn (evar_conv_x ts) env evd
+ (position_problem true pbty,ev,term2) with
+ | UnifFailure (_, Pretype_errors.OccurCheck _) -> default ()
+ | x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) ->
- solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem false pbty,ev,term1)
- | _ ->
- evar_eqappr_x ts env evd pbty
- (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
- (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+ (match solve_simple_eqn (evar_conv_x ts) env evd
+ (position_problem false pbty,ev,term1) with
+ | UnifFailure (_, Pretype_errors.OccurCheck _) -> default ()
+ | x -> x)
+ | _ -> default ()
end
and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
@@ -338,13 +343,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in
let miller_pfenning on_left fallback ev lF apprM evd =
let tM = Stack.zip apprM in
- match is_unification_pattern_evar env evd ev lF tM with
+ let cont res =
+ match res with
| None -> fallback ()
| Some l1' -> (* Miller-Pfenning's patterns unification *)
let t2 = nf_evar evd tM in
let t2 = solve_pattern_eqn env l1' t2 in
- solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem on_left pbty,ev,t2) in
+ solve_simple_eqn (evar_conv_x ts) env evd
+ (position_problem on_left pbty,ev,t2)
+ in
+ try cont (is_unification_pattern_evar_occur env evd ev lF tM)
+ with Occur -> UnifFailure (evd,OccurCheck (fst ev,tM))
+ in
let consume_stack on_left (termF,skF) (termO,skO) evd =
let switch f a b = if on_left then f a b else f b a in
let not_only_app = Stack.not_purely_applicative skO in
@@ -407,9 +417,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ev lF apprR evd
in
let f2 evd =
- if isLambda termR then
- eta env evd false skR termR skF termF
- else UnifFailure (evd,NotSameHead)
+ match kind_of_term termR with
+ | Lambda _ -> eta env evd false skR termR skF termF
+ | Construct u -> eta_constructor ts env evd skR u skF termF
+ | _ -> UnifFailure (evd,NotSameHead)
in ise_try evd [f1;f2] in
let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
(* Evar must be undefined since we have flushed evars *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 08b704bdea..14bc45e0ce 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -418,16 +418,23 @@ let is_unification_pattern_meta env nb m l t =
else
None
-let is_unification_pattern_evar env evd (evk,args) l t =
- if List.for_all (fun x -> isRel x || isVar x) l && noccur_evar env evd evk t
+let is_unification_pattern_evar_occur env evd (evk,args) l t =
+ if List.for_all (fun x -> isRel x || isVar x) l
then
- let args = remove_instance_local_defs evd evk args in
- let n = List.length args in
- match find_unification_pattern_args env (args @ l) t with
- | Some l -> Some (List.skipn n l)
- | _ -> None
+ if not (noccur_evar env evd evk t) then raise Occur
+ else
+ let args = remove_instance_local_defs evd evk args in
+ let n = List.length args in
+ match find_unification_pattern_args env (args @ l) t with
+ | Some l -> Some (List.skipn n l)
+ | _ -> None
else
- None
+ if noccur_evar env evd evk t then None
+ else raise Occur
+
+let is_unification_pattern_evar env evd ev l t =
+ try is_unification_pattern_evar_occur env evd ev l t
+ with Occur -> None
let is_unification_pattern_pure_evar env evd (evk,args) t =
let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index e35fb44b15..a0d0f6fdf6 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -51,6 +51,10 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+(** Raises [Occur] if the evar occurs in the evar-expanded version of the term. *)
+val is_unification_pattern_evar_occur : env -> evar_map -> existential -> constr list ->
+ constr -> constr list option
+
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> constr list option
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2a0b6fd18..a2791f7a20 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -930,10 +930,10 @@ let simpl env sigma c = strong whd_simpl env sigma c
(* Reduction at specific subterms *)
-let matches_head c t =
+let matches_head env sigma c t =
match kind_of_term t with
- | App (f,_) -> ConstrMatching.matches c f
- | Proj (p, _) -> ConstrMatching.matches c (mkConst p)
+ | App (f,_) -> ConstrMatching.matches env sigma c f
+ | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst p)
| _ -> raise ConstrMatching.PatternMatchingFailure
let e_contextually byhead (occs,c) f env sigma t =
@@ -946,7 +946,8 @@ let e_contextually byhead (occs,c) f env sigma t =
else
try
let subst =
- if byhead then matches_head c t else ConstrMatching.matches c t in
+ if byhead then matches_head env sigma c t
+ else ConstrMatching.matches env sigma c t in
let ok =
if nowhere_except_in then Int.List.mem !pos locs
else not (Int.List.mem !pos locs) in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e7082a579f..418fc62f0c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1218,16 +1218,20 @@ si après Intros la conclusion matche le pattern.
let (forward_interp_tactic, extern_interp) = Hook.make ()
let conclPattern concl pat tac =
- let constr_bindings =
+ let constr_bindings env sigma =
match pat with
| None -> Proofview.tclUNIT Id.Map.empty
| Some pat ->
- try Proofview.tclUNIT (ConstrMatching.matches pat concl)
+ try
+ Proofview.tclUNIT (ConstrMatching.matches env sigma pat concl)
with ConstrMatching.PatternMatchingFailure ->
Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
in
- constr_bindings >>= fun constr_bindings ->
- Hook.get forward_interp_tactic constr_bindings tac
+ Proofview.Goal.raw_enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ constr_bindings env sigma >>= fun constr_bindings ->
+ Hook.get forward_interp_tactic constr_bindings tac)
(***********************************************************)
(** A debugging / verbosity framework for trivial and auto *)
@@ -1461,7 +1465,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
if exists_evaluable_reference (pf_env gl) c then
tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
else tclFAIL 0 (str"Unbound reference") gl)
- | Extern tacast -> conclPattern concl p tacast
+ | Extern tacast ->
+ conclPattern concl p tacast
in
tclLOG dbg (fun () -> pr_autotactic t) tactic
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index e171c21474..84fcd6dee1 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -245,6 +245,9 @@ let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
open Globnames
+let is_matching x y = is_matching (Global.env ()) Evd.empty x y
+let matches x y = matches (Global.env ()) Evd.empty x y
+
let match_with_equation t =
if not (isApp t) then raise NoEquationFound;
let (hdapp,args) = destApp t in
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index 0f48db6766..fa1b7f1586 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -228,7 +228,7 @@ module PatternMatching (E:StaticEnvironment) = struct
| Term p ->
begin
try
- put_subst (ConstrMatching.extended_matches p term) <*>
+ put_subst (ConstrMatching.extended_matches E.env E.sigma p term) <*>
return lhs
with ConstrMatching.PatternMatchingFailure -> fail
end
@@ -247,7 +247,7 @@ module PatternMatching (E:StaticEnvironment) = struct
| Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
}
in
- map (ConstrMatching.match_subterm_gen with_app_context p term) matching_error
+ map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error
(** [rule_match_term term rule] matches the term [term] with the
diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/closed/3377.v
index 23c0a965c8..8e9e3933cc 100644
--- a/test-suite/bugs/opened/3377.v
+++ b/test-suite/bugs/closed/3377.v
@@ -4,6 +4,14 @@ Record prod A B := pair { fst : A; snd : B}.
Goal fst (@pair Type Type Type Type).
Set Printing All.
-Fail match goal with |- ?f _ => idtac end.
+match goal with |- ?f ?x => set (foo := f x) end.
+
+Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x).
+Proof.
+ intro x.
+ lazymatch goal with
+ | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f
+ end.
+
(* Toplevel input, characters 7-44:
Error: No matching clauses for match. *)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index e2a4ad25cf..6a7d2c8118 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -98,7 +98,7 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env typ =
let typ = strip_outer_cast typ in
- if ConstrMatching.is_matching pat typ then true
+ if ConstrMatching.is_matching env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
@@ -106,7 +106,7 @@ let rec pattern_filter pat ref env typ =
let rec head_filter pat ref env typ =
let typ = strip_outer_cast typ in
- if ConstrMatching.is_matching_head pat typ then true
+ if ConstrMatching.is_matching_head env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> head_filter pat ref env typ
@@ -135,7 +135,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
let search_about_filter query gr env typ = match query with
| GlobSearchSubPattern pat ->
- ConstrMatching.is_matching_appsubterm ~closed:false pat typ
+ ConstrMatching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
| GlobSearchString s ->
String.string_contains ~where:(name_of_reference gr) ~what:s
@@ -274,11 +274,12 @@ let interface_search flags =
toggle (Str.string_match regexp id 0) flag
in
let match_type (pat, flag) =
- toggle (ConstrMatching.is_matching pat constr) flag
+ toggle (ConstrMatching.is_matching env Evd.empty pat constr) flag
in
let match_subtype (pat, flag) =
toggle
- (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag
+ (ConstrMatching.is_matching_appsubterm ~closed:false
+ env Evd.empty pat constr) flag
in
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:31:10 +0000