diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-26 12:31:25 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-26 12:31:25 +0000 |
commit | fc10282837971f8f0648841d944dd64b11d3a3db (patch) | |
tree | 284365ebab8674ad5079eaf662a7de1f3eb2909c /pretyping/coercion.ml | |
parent | c48117086c36e328d37a0400a4bda72d1537554f (diff) |
- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec
"pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bd023721a..5a99adb5a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -160,7 +160,7 @@ module Default = struct let inh_coerce_to_base loc env evd j = (evd, j) - let inh_coerce_to_fail env evd rigidonly v c1 t = + let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) then raise NoCoercion @@ -183,7 +183,7 @@ module Default = struct let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) with Reduction.NotConvertible -> - try inh_coerce_to_fail env evd rigidonly v c1 t + try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match kind_of_term (whd_betadeltaiota env (evars_of evd) t), |