aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/subtac/subtac_cases.ml2
-rw-r--r--contrib/subtac/subtac_coercion.ml33
2 files changed, 21 insertions, 14 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6a470afc6..45f0f0129 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1977,7 +1977,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
(lift (nargeqs + nar) arg),
mk_eq_refl argt arg)
else
- (mk_JMeq (lift (nargeqs + slift) appt)
+ (mk_JMeq (lift (nargeqs + slift) t)
(mkRel (nargeqs + slift))
(lift (nargeqs + nar) argt)
(lift (nargeqs + nar) arg),
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 5ca313d0b..4a1869053 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -129,9 +129,9 @@ module Coercion = struct
with Reduction.NotConvertible -> coerce' env x y
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- let rec coerce_application typ c c' l l' =
+ let rec coerce_application typ typ' c c' l l' =
let len = Array.length l in
- let rec aux tele typ i co =
+ let rec aux tele typ typ' i co =
(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
(* str " to "++ my_print_constr env y *)
(* ++ str "in env:" ++ my_print_env env); *)
@@ -140,9 +140,15 @@ module Coercion = struct
let hdx = l.(i) and hdy = l'.(i) in
try isevars := the_conv_x_leq env hdx hdy !isevars;
let (n, eqT, restT) = destProd typ in
- aux (hdx :: tele) (subst1 hdy restT) (succ i) co
+ let (n', eqT', restT') = destProd typ' in
+ aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
with Reduction.NotConvertible ->
let (n, eqT, restT) = destProd typ in
+ let (n', eqT', restT') = destProd typ' in
+ let _ =
+ try isevars := the_conv_x_leq env eqT eqT' !isevars
+ with Reduction.NotConvertible -> raise NoSubtacCoercion
+ in
let restargs = lift_args 1
(List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
in
@@ -154,9 +160,9 @@ module Coercion = struct
let eq_app x = mkApp (Lazy.force eq_rect,
[| eqT; hdx; pred; x; hdy; evar|]) in
(* trace (str"Inserting coercion at application"); *)
- aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
- else co
- in aux [] typ 0 (fun x -> x)
+ aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
+ else Some co
+ in aux [] typ typ' 0 (fun x -> x)
in
(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
(* str " to "++ my_print_constr env y *)
@@ -264,21 +270,22 @@ module Coercion = struct
else
if i = i' && len = Array.length l' then
let evm = evars_of !isevars in
- let typ = Typing.type_of env evm c in
(try subco ()
- with NoSubtacCoercion ->
-
-(* if not (is_arity env evm typ) then *)
- Some (coerce_application typ c c' l l'))
-(* else subco () *)
+ with NoSubtacCoercion ->
+ let typ = Typing.type_of env evm c in
+ let typ' = Typing.type_of env evm c' in
+ (* if not (is_arity env evm typ) then *)
+ coerce_application typ typ' c c' l l')
+ (* else subco () *)
else
subco ()
| x, y when x = y ->
if Array.length l = Array.length l' then
let evm = evars_of !isevars in
let lam_type = Typing.type_of env evm c in
+ let lam_type' = Typing.type_of env evm c' in
(* if not (is_arity env evm lam_type) then ( *)
- Some (coerce_application lam_type c c' l l')
+ coerce_application lam_type lam_type' c c' l l'
(* ) else subco () *)
else subco ()
| _ -> subco ())