diff options
| author | Maxime Dénès | 2018-09-12 17:12:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-12 17:12:20 +0200 |
| commit | 60103f4af881485c0f905ebcb6710b31744466d0 (patch) | |
| tree | 42c9f735a4904f7c97b8b47368c04c1a9eccc1c9 /engine/evd.ml | |
| parent | e3e1f56c38f345bccf984dd6d6d86fa06e423b96 (diff) | |
| parent | 55a328bb38f112cf2f456de4f1d9fc1bccaf88b1 (diff) | |
Merge PR #7109: Term combinators respecting the canonical structure of branches and return predicate
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 9f976b57dd..d7b03a84f1 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1267,7 +1267,9 @@ module MiniEConstr = struct let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind let of_constr c = c + let of_constr_array v = v let unsafe_to_constr c = c + let unsafe_to_constr_array v = v let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = |