diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:30 +0000 |
| commit | 2833dc95391a2eaf2c48cb7febac6eec8f07bfa4 (patch) | |
| tree | d723c16bd45204974135a860a7040db10600d81c | |
| parent | 2118e320c272d88d01eab650e0dd0e83597230e1 (diff) | |
Added support for instantiation of ?n by a lambda when "?n a" has to
be unified with a (truly) rigid term.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13883 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3906f8728..8b7fde3c2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -374,7 +374,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let appr2 = evar_apprec env' evd [] c'2 in evar_eqappr_x ts env' evd CONV appr1 appr2 - | Flexible ev1, (Rigid _ | PseudoRigid _) -> + | Flexible ev1, (Rigid _ | PseudoRigid _ as c2) -> if is_unification_pattern_evar env ev1 l1 (applist appr2) & not (occur_evar (fst ev1) (applist appr2)) @@ -385,12 +385,16 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let t2 = solve_pattern_eqn env l1 t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem true pbty,ev1,t2) + else if is_rigid c2 & l1 <> [] then + let (evd',c1) = define_evar_as_lambda env evd ev1 in + evar_eqappr_x ts env evd' pbty + (decompose_app (beta_applist (c1,l1))) appr2 else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true - | (Rigid _ | PseudoRigid _), Flexible ev2 -> + | (Rigid _ | PseudoRigid _ as c1), Flexible ev2 -> if is_unification_pattern_evar env ev2 l2 (applist appr1) & not (occur_evar (fst ev2) (applist appr1)) @@ -401,6 +405,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let t1 = solve_pattern_eqn env l2 t1 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem false pbty,ev2,t1) + else if is_rigid c1 & l2 <> [] then + let (evd',c2) = define_evar_as_lambda env evd ev2 in + evar_eqappr_x ts env evd' pbty appr1 + (decompose_app (beta_applist (c2,l2))) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, |