aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-30 15:54:12 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-30 15:54:12 +0100
commit0bb126dae41b410fdf4f6531024c64cac20dac06 (patch)
treecc3a9c0d8133eae3902b3a441246d50c48f02436 /tactics
parentee45637ac2431fe2df1994f2337d8801e2aeff9a (diff)
parent08da05299d32886bb516124fa497347b40249006 (diff)
Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes #3125)
Diffstat (limited to 'tactics')
-rw-r--r--tactics/equality.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c36ad980e..0d6263246 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -739,7 +739,7 @@ let keep_proof_equalities = function
let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
- let s = get_sort_family_of env sigma ty1 in
+ let s = get_sort_family_of ~truncation_style:true env sigma ty1 in
if Sorts.List.mem s sorts
then [(List.rev posn,t1,t2)] else []
in