From f4a8b00fa0ca47ef7dce4ca2ca809ef4ac440d38 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Nov 2014 19:56:00 +0100 Subject: Experimenting using unification when matching evar/meta free subterms while before these were supposed to consider only syntactically. Made the experiment to unify with all delta flags unset. Keeping the same flags as for non evar/meta free subterms would lead to too much successes, as e.g. "true && b" matching "b" when the modulo_conv_on_closed_terms flag is set, which is the case for rewrite. But maybe should we instead investigate to have the same flags but with the restrict_conv_on_strict_subterms flag set. This rules out examples like "true && b" unifying with "b" and this is another option which is ok for compiling the stdlib without any changes. --- test-suite/success/rewrite.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index f7b9897c1..6dcd6592b 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -139,3 +139,12 @@ subst z. rewrite H0. auto with arith. Qed. + +(* Check that evars are instantiated when the term to rewrite is + closed, like in the case it is open *) + +Goal exists x, S 0 = 0 -> S x = 0. +eexists. intro H. +rewrite H. +reflexivity. +Abort. -- cgit v1.2.3