diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 14:58:46 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 14:58:46 +0200 |
commit | 8e9d08f99c2058ed03df6b0135ec1661130e85e5 (patch) | |
tree | cff735811cf0c4faf9462b4464a1f42e57062f14 /pretyping/tacred.ml | |
parent | dfbf22a098e8e2890d2e10da5d669d9960ef6771 (diff) | |
parent | fc13ad4128b2d75a459829556669a59c10e8e1fe (diff) |
Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.
Diffstat (limited to 'pretyping/tacred.ml')
0 files changed, 0 insertions, 0 deletions