From b25bdeaed71fdd823262f74ae6ed3935d3322e9f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 3 Apr 2019 10:22:13 +0000 Subject: [Micromega] Use EConstr.eq_constr_universes_proj --- doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst new file mode 100644 index 0000000000..d6fc724415 --- /dev/null +++ b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst @@ -0,0 +1,4 @@ +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 `_, + fixes `#9512 `_ + by Vincent Laporte). -- cgit v1.2.3