Added full pattern-unification on Meta for tactic unification.

No way to control it yet; maybe flag use_evars_pattern_unification
should be generalized for that purpose.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 44 insertions, 10 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8c0c21046f..d7013aca8f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1285,8 +1285,8 @@ let is_unification_pattern_evar env (_,args) l t =
 let is_unification_pattern (env,nb) f l t =
   match kind_of_term f with
     | Meta _ ->
-	array_for_all (fun c -> isRel c && destRel c <= nb) l
-	&& array_distinct l
+	let dummy_ev = (f,[||]) in
+	is_unification_pattern_evar env dummy_ev (Array.to_list l) t
     | Evar ev ->
 	is_unification_pattern_evar env ev (Array.to_list l) t
     | _ ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index cd848984d4..dfc1e2f896 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -282,6 +282,16 @@ let decompose_app_vect c =
   | App (f,cl) -> (f, cl)
   | _ -> (c,[||])
 
+let adjust_app_list_size f1 l1 f2 l2 =
+  let len1 = List.length l1 and len2 = List.length l2 in
+  if len1 = len2 then (f1,l1,f2,l2)
+  else if len1 < len2 then
+   let extras,restl2 = list_chop (len2-len1) l2 in
+    (f1, l1, applist (f2,extras), restl2)
+  else
+    let extras,restl1 = list_chop (len1-len2) l1 in
+    (applist (f1,extras), restl1, f2, l2)
+
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
    list) which is processed by [g na] (which typically cons [na] to
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 71e781aeb8..c6ca30407f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -201,6 +201,9 @@ val last_arg : constr -> constr
 (** Force the decomposition of a term as an applicative one *)
 val decompose_app_vect : constr -> constr * constr array
 
+val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
+  (constr * constr list * constr * constr list)
+
 (** name contexts *)
 type names_context = name list
 val add_name : name -> names_context -> names_context
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c233674aec..bf03da8bdb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -231,6 +231,9 @@ let elim_no_delta_flags = {
   allow_K_in_toplevel_higher_order_unification = true
 }
 
+let set_no_head_reduction flags =
+  { flags with restrict_conv_on_strict_subterms = true }
+
 let use_evars_pattern_unification flags =
   !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification
   && Flags.version_strictly_greater Flags.V8_2
@@ -837,6 +840,14 @@ let check_types env flags (sigma,_,_ as subst) m n =
       (get_type_of env sigma n)
   else subst
 
+let try_resolve_typeclasses env evd flags m n =
+  if flags.resolve_evars then
+    try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+	  ~fail:true env evd
+    with e when Typeclasses_errors.unsatisfiable_exception e ->
+      error_cannot_unify env evd (m, n)
+  else evd
+
 let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
@@ -844,16 +855,19 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
      unify_0_with_initial_metas (evd',ms,es) false env cv_pb flags m n
   in
   let evd = w_merge env with_types flags subst2 in
-    if flags.resolve_evars then
-      try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
-	~fail:true env evd
-      with e when Typeclasses_errors.unsatisfiable_exception e ->
-	error_cannot_unify env evd (m, n)
-    else evd
+  try_resolve_typeclasses env evd flags m n
 
 let w_unify_0 env = w_unify_core_0 env false
 let w_typed_unify env = w_unify_core_0 env true
 
+let w_typed_unify_list env cv_pb flags f1 l1 f2 l2 evd =
+  let flags' = { flags with resolve_evars = false } in
+  let f1,l1,f2,l2 = adjust_app_list_size f1 l1 f2 l2 in
+  let evd =
+    List.fold_left2 (fun evd m n ->
+      w_unify_core_0 env true cv_pb flags' m n evd) evd (f1::l1) (f2::l2) in
+  try_resolve_typeclasses env evd flags (applist(f1,l1)) (applist(f2,l2))
+
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
    FAIL because we cannot find a binding *)
@@ -1068,7 +1082,7 @@ let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
 	  when List.length l1 = List.length l2 ->
 	  (try
-	      w_typed_unify env cv_pb flags ty1 ty2 evd
+	      w_typed_unify_list env cv_pb flags hd1 l1 hd2 l2 evd
 	    with ex when precatchable_exception ex ->
 	      try
 		w_unify2 env flags cv_pb ty1 ty2 evd
@@ -1081,7 +1095,7 @@ let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	    with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
 	      | ex when precatchable_exception ex ->
 		  try
-		    w_typed_unify env cv_pb flags ty1 ty2 evd
+		    w_typed_unify_list env cv_pb flags hd1 l1 hd2 l2 evd
 		  with ex' when precatchable_exception ex' ->
 		    raise ex)
 
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 18ba0fc870..fdc7c72220 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -21,6 +21,12 @@ Proof.
 intros; apply H.
 Qed.
 
+  (* Feature introduced June 2011 *)
+
+Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
+Proof.
+intros x P H; apply H.
+Qed.
 
 (* Example submitted for Zenon *)
 
@@ -138,3 +144,4 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
 Proof.
   intros.
   rewrite H with (f:=f0).
+Abort.