aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/unification.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1a1d03cc8a..07940bf57d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1480,7 +1480,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
++ str ".")
else
(push_named_context_val d sign,depdecls)
- | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ ->
+ | (AtOccs (AllOccurrences, InHyp) | LikeFirst) ->
let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in
if Context.eq_named_declaration d newdecl
&& not (indirectly_dependent c d depdecls)