diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-17 16:52:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-17 16:53:15 +0200 |
| commit | 77df7b1283940d979d3e14893d151bc544f41410 (patch) | |
| tree | f8762ff000264c00bb9e870c5acb3ac02faea411 /pretyping/coercion.ml | |
| parent | 39e8010bf51b687f11d04c6a44cb959e85e86f7b (diff) | |
Fix coercion code to disallow using cumulativity in the domain of products, which
results in strange changes in user provided terms.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index dfaff327a..3b82e52a3 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -445,8 +445,10 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = - try (the_conv_x_leq env t c1 evd, v) +let rec inh_conv_coerce_to_fail ?(cumul=true) loc env evd rigidonly v t c1 = + try if cumul then + (the_conv_x_leq env t c1 evd, v) + else (the_conv_x env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> @@ -466,7 +468,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = | _ -> name in let env1 = push_rel (name,None,u1) env in let (evd', v1) = - inh_conv_coerce_to_fail loc env1 evd rigidonly + inh_conv_coerce_to_fail ~cumul:false loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in |