diff options
| -rw-r--r-- | dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh | 6 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 4 | ||||
| -rw-r--r-- | pretyping/constr_matching.mli | 2 |
4 files changed, 10 insertions, 4 deletions
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 000000000..517088a24 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c810..c949589e2 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a41..b4e1a1b10 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -427,7 +427,7 @@ let special_meta = (-1) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } + m_ctx : constr Lazy.t; } let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) @@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx = let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) - else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next) with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915..d19789ef4 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], |