From c221e1bebd5fabe7c5995c9306b96596026de047 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 Jul 2009 12:30:19 +0000
Subject: Reactivation of pattern unification of evars in apply unification, in
 agreement with wish #2117 (pattern unification of evars remained deactivated
 for 3 years because of incompatibilities with eauto [see commit 9234]; thanks
 to unification flags, it can be activated for apply w/o changing eauto). Also
 add test for bug #2123 (see commit 12228).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml  | 9 +++++++--
 pretyping/unification.mli | 1 +
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8ea2eae11b..0846359a85 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -128,6 +128,7 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
+  use_evars_pattern_unification : bool
 }
 
 let default_unify_flags = {
@@ -135,6 +136,7 @@ let default_unify_flags = {
   use_metas_eagerly = true;
   modulo_delta = full_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let default_no_delta_unify_flags = {
@@ -142,6 +144,7 @@ let default_no_delta_unify_flags = {
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let expand_key env = function
@@ -229,12 +232,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		  (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
 
 	| App (f1,l1), _ when
-	    isMeta f1 & is_unification_pattern curenvnb f1 l1 cN &
+	    (isMeta f1 || flags.use_evars_pattern_unification && isEvar f1) &
+	    is_unification_pattern curenvnb f1 l1 cN &
 	    not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
 
 	| _, App (f2,l2) when
-	    isMeta f2 & is_unification_pattern curenvnb f2 l2 cM &
+	    (isMeta f2 || flags.use_evars_pattern_unification && isEvar f2) &
+	    is_unification_pattern curenvnb f2 l2 cM &
 	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8d71ec4bd6..43c9dd2e9b 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -19,6 +19,7 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
+  use_evars_pattern_unification : bool
 }
 
 val default_unify_flags : unify_flags
-- 
cgit v1.2.3