diff options
| author | herbelin | 2006-03-02 17:23:41 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-02 17:23:41 +0000 |
| commit | 4ac83a8cc2a43a20152454f58d9401d4fa9c87a4 (patch) | |
| tree | 707884085b9e3e40c80ee9956f8a3ee90bc5c960 | |
| parent | 9b0be87644b7d636c0df4207678c393d9ff68e85 (diff) | |
Correctif pour bug #1089 (cannot define an isevar twice)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8111 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9f9cc46a66..2c5a0f9015 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -300,8 +300,13 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and isevars (* First compare extra args for better failure message *) [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2); - (fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev1,applist(term2,deb2)))] + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t2 = applist(term2,deb2) in + if is_defined_evar i ev1 then + evar_conv_x env i pbty (mkEvar ev1) t2 + else + solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] else (isevars,false) | Rigid _, Flexible ev2 -> if List.length l2 <= List.length l1 then @@ -309,8 +314,13 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and isevars (* First compare extra args for better failure message *) [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2); - (fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev2,applist(term1,deb1)))] + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t1 = applist(term1,deb1) in + if is_defined_evar i ev2 then + evar_conv_x env i pbty t1 (mkEvar ev2) + else + solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))] else (isevars,false) | MaybeFlexible flex1, Rigid _ -> |