diff options
| author | Pierre-Marie Pédrot | 2018-05-15 16:18:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-15 16:18:58 +0200 |
| commit | 7db66596d71759a94c090e2cb0735df4809beaa4 (patch) | |
| tree | 21d66143eb783b21e71d10b7b4ff4548a00bc01f | |
| parent | 51cac34f4c72d318570078fb52a5bfff27e59fa9 (diff) | |
| parent | a255ba63f82652ac7dae4a39e80c35f813d0e5a3 (diff) | |
Merge branch 'fast-constr-match-no-context'
| -rw-r--r-- | src/tac2core.ml | 4 | ||||
| -rw-r--r-- | src/tac2match.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 32c873088c..9a3aed3442 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -557,7 +557,7 @@ let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c -> | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) -> let ans = Id.Map.bindings sub in let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in - let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list of_pair ans |] in + let ans = Value.of_tuple [| Value.of_constr (Lazy.force m_ctx); Value.of_list of_pair ans |] in Proofview.tclOR (return ans) (fun _ -> of_ans s) in pf_apply begin fun env sigma -> @@ -589,7 +589,7 @@ let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c - | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) -> let ans = Id.Map.bindings sub in let ans = Array.map_of_list snd ans in - let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_array Value.of_constr ans |] in + let ans = Value.of_tuple [| Value.of_constr (Lazy.force m_ctx); Value.of_array Value.of_constr ans |] in Proofview.tclOR (return ans) (fun _ -> of_ans s) in pf_apply begin fun env sigma -> diff --git a/src/tac2match.ml b/src/tac2match.ml index 5035c9dba6..a3140eabea 100644 --- a/src/tac2match.ml +++ b/src/tac2match.ml @@ -170,7 +170,7 @@ module PatternMatching (E:StaticEnvironment) = struct let nctx = { subst } in match merge ctx nctx with | None -> (map s (e, info)).stream k ctx - | Some nctx -> Proofview.tclOR (k (Some m_ctx) nctx) (fun e -> (map s e).stream k ctx) + | Some nctx -> Proofview.tclOR (k (Some (Lazy.force m_ctx)) nctx) (fun e -> (map s e).stream k ctx) } in map (Constr_matching.match_subterm E.env E.sigma (Id.Set.empty,p) term) imatching_error |