diff options
| author | Hugo Herbelin | 2020-09-03 11:44:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-03 11:44:40 +0200 |
| commit | 8cd66c83327093ec90f8b7d489cd4bd62d92e5f2 (patch) | |
| tree | 60ece61b3b9f8614283c81405fdaedca4e168cdb /tactics/tactics.ml | |
| parent | ce0c1475badd3ceef940db1fab965128cd752e6a (diff) | |
| parent | 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 (diff) | |
Merge PR #12973: Random cleanup around the data structures used in Equality
Reviewed-by: herbelin
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e2d60dfabd..5f7e35d205 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function |