diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-25 18:12:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 13:41:26 +0200 |
| commit | c538b7fd555828d9fba9ea97503fac6c70377b76 (patch) | |
| tree | 07e78f71124cb0ba6d6d69137df838f179e11571 /plugins/ssrmatching | |
| parent | 864fda19d046428023851ba540b82c5ca24d06a4 (diff) | |
Convert clear_hyps_in_evi to state passing style.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a10437a63..0dd3625ba 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1099,15 +1099,14 @@ let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - let evdref = ref (Evd.clear_metas sigma) in + let sigma = Evd.clear_metas sigma in let ans = - try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) + try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids) with Evarutil.ClearDependencyError _ -> None in match ans with | None -> sigma - | Some (hyps, concl) -> - let sigma = !evdref in + | Some (sigma, hyps, concl) -> let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma |