diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:49:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 22:04:41 +0100 |
| commit | 08da05299d32886bb516124fa497347b40249006 (patch) | |
| tree | 14d186a8ae04c09ab6f1e13eb0e204a7b5867519 /tactics/equality.ml | |
| parent | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (diff) | |
In injection/inversion, consider all template-polymorphic types as injectable.
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 2 |
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 |