diff options
| author | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
| commit | da58ae4c620412923ea84b1982e8765f6be145a8 (patch) | |
| tree | 8518269959c007a7c70bdbd80a968ebff03c6415 /vernac | |
| parent | 3bc0c82700a805e889198b810cc0148f6479cbe1 (diff) | |
| parent | 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 (diff) | |
Merge PR #7912: Simplify effects API
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ce74f2344a..880a11becd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in + let fold env eff = + try + let _ = Environ.lookup_constant eff.seff_constant env in + env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard env possible_indexes fixdecls in |