diff options
| author | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
| commit | 3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch) | |
| tree | 34f2b0419b52861cb83bb42a90728161c7f792b4 /pretyping/unification.ml | |
| parent | d6175b9980808ff91f1299ca26a9a49a117169ca (diff) | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
Merge branch 'master' into econstr
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index eb90dfbdb6..532cc8baa5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1571,7 +1571,7 @@ let default_matching_merge_flags sigma = use_pattern_unification = true; } -let default_matching_flags (sigma,_) = +let default_matching_flags sigma = let flags = default_matching_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = default_matching_merge_flags sigma; @@ -1709,10 +1709,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool -type pending_constr = Evd.pending * constr - type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type 'r abstraction_result = |