diff options
| author | Pierre-Marie Pédrot | 2018-04-11 08:30:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-11 08:30:56 +0200 |
| commit | a255ba63f82652ac7dae4a39e80c35f813d0e5a3 (patch) | |
| tree | 07c9937f95cc1ac2112ccf52c1d7c697dd09aeef /src | |
| parent | 67157b85f2bd4e6e6e23945686043e3479e39d67 (diff) | |
Fix compilation w.r.t. coq/coq#7213.
Diffstat (limited to 'src')
| -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 |