From 6f3400ed7f6aa2810d72f803273f04a7add04207 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Mar 2008 11:23:13 +0000
Subject: Toujours suite commits 10623 et 10624: - l'occur-check doit être fait
 aussi quand on imite, - pour simplifier et en se basant sur les commentaires
 antérieurs à   1995 (de Chet?) et parlant de mimick_evar, on restreint
 l'appel à   mimick_evar au cas où l'instance contient des Meta.

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0869bfb020..1741d7fea7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -445,14 +445,12 @@ let w_merge env with_types flags metas evars evd =
     	else begin
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
-	  | App (f,cl) when is_mimick_head f ->
-	      let evd' = solve_simple_evar_eqn env evd ev rhs' in
-	      (try w_merge_rec evd' metas evars' eqns
-	       with ex when precatchable_exception ex ->
-               let evd' = mimick_evar evd flags f (Array.length cl) evn in
-	       w_merge_rec evd' metas evars eqns)
+	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
+	      if occur_evar evn rhs' then
+                error_occur_check env (evars_of evd) evn rhs';
+	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
+	      w_merge_rec evd' metas evars eqns
           | _ ->
-              (* ensure tail recursion in non-mimickable case! *)
 	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs') 
 	        metas evars' eqns
 	  end
-- 
cgit v1.2.3