diff options
| author | Frédéric Besson | 2020-08-10 15:31:58 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-08-10 15:35:30 +0200 |
| commit | 4da8f114155d2abb31ce8a45a2f17f21f7d97a0e (patch) | |
| tree | b271937251f65b7e454d67c2cca97687b24766fd | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
[zify] fix for bug#12791
The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
| -rw-r--r-- | plugins/micromega/zify.ml | 11 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12791.v | 9 |
2 files changed, 17 insertions, 3 deletions
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 4e1f9a66ac..fa29e6080e 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) = let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in try - ignore (get_injection env evd (EConstr.of_constr ty)); - tac id.Context.binder_name (EConstr.of_constr t) - (EConstr.of_constr ty) + let x = id.Context.binder_name in + ignore + (let eq = Lazy.force eq in + find_option + (match_operator env evd eq + [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|]) + (HConstr.find_all eq !table_cache)); + tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) let iter_let_aux tac = diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. |