From 90069c14ff393c33efdf7477bda096f5ba684bc1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 6 Mar 2008 08:22:58 +0000 Subject: Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n dans certains cas. Branchement au passage de w_unify vers evar_conv et solve_simple_eqn en cas d'équations entre Evars. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 890f0bd78..d4cd9d6ea 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -420,6 +420,12 @@ let order_metas metas = else meta :: order latemetas metas in order [] metas +(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) + +let solve_simple_evar_eqn env evd ev rhs = + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + if b then evd else error_cannot_unify env (evars_of evd) (mkEvar ev,rhs) + (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] is true, unification of types of metas is required *) @@ -437,11 +443,10 @@ let w_merge env with_types flags metas evars evd = w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin let rhs' = subst_meta_instances metas rhs in - if occur_evar evn rhs' then error "w_merge: recursive equation"; match kind_of_term rhs with | App (f,cl) when is_mimick_head f -> (try - w_merge_rec (evar_define env ev rhs' evd) + w_merge_rec (solve_simple_evar_eqn env evd ev rhs') metas evars' eqns with ex when precatchable_exception ex -> let evd' = @@ -449,7 +454,8 @@ let w_merge env with_types flags metas evars evd = w_merge_rec evd' metas evars eqns) | _ -> (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (evar_define env ev rhs' evd) metas evars' eqns + w_merge_rec (solve_simple_evar_eqn env evd ev rhs') + metas evars' eqns end | [] -> -- cgit v1.2.3