From 87722d2a5d9592f08fafa2b4d56c9ba7aadd1033 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Sep 2006 10:35:13 +0000
Subject: Correction conflit Meta/Evar dans commit précédent et extension au
 passage de l'unification pattern au cas tant des Meta que des Evar.

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index dab4b4f12f..abdf8c863f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,7 +49,13 @@ let abstract_list_all env sigma typ c l =
 
 (**)
 
-let solve_pattern_eqn_array env l c = solve_pattern_eqn env (Array.to_list l) c
+let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
+  match kind_of_term f with
+    | Meta k -> 
+	(k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst
+    | Evar ev ->
+	metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+    | _ -> assert false
 
 (*******************************)
 
@@ -100,12 +106,10 @@ let unify_0 env sigma cv_pb mod_delta m n =
       | App (f1,l1), App (f2,l2) ->
 	  if is_unification_pattern f1 l1 & not (dependent f1 cN)
 	  then
-	    (destMeta f1,solve_pattern_eqn_array env l1 cN)::metasubst,
-	    evarsubst
+	    solve_pattern_eqn_array env f1 l1 cN substn
 	  else if is_unification_pattern f2 l2 & not (dependent f2 cM)
 	  then
-	    (destMeta f2,solve_pattern_eqn_array env l2 cM)::metasubst,
-	    evarsubst
+	    solve_pattern_eqn_array env f2 l2 cM substn
 	  else
 	  let len1 = Array.length l1
 	  and len2 = Array.length l2 in
-- 
cgit v1.2.3