diff options
| -rw-r--r-- | .depend.coq | 1 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | contrib/subtac/SubtacTactics.v (renamed from contrib/subtac/Tactics.v) | 0 | ||||
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 51 |
4 files changed, 23 insertions, 31 deletions
diff --git a/.depend.coq b/.depend.coq index 2b627f7c2..c09410497 100644 --- a/.depend.coq +++ b/.depend.coq @@ -362,6 +362,7 @@ contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo +contrib/subtac/SubtacTactics.vo: contrib/subtac/SubtacTactics.v contrib/subtac/Utils.vo: contrib/subtac/Utils.v theories/Logic/ProofIrrelevance.vo contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo contrib/subtac/Utils.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo contrib/subtac/Subtac.vo: contrib/subtac/Subtac.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo @@ -1101,7 +1101,7 @@ JPROVERVO= CCVO= -SUBTACVO=contrib/subtac/Tactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ +SUBTACVO=contrib/subtac/SubtacTactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ contrib/subtac/FunctionalExtensionality.vo RTAUTOVO = \ diff --git a/contrib/subtac/Tactics.v b/contrib/subtac/SubtacTactics.v index 25d8d8319..25d8d8319 100644 --- a/contrib/subtac/Tactics.v +++ b/contrib/subtac/SubtacTactics.v diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 30fd8281e..38a95e9bc 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -122,6 +122,22 @@ module Coercion = struct with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars 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 aux typ i co = + trace (str"Inserting coercion at application"); + if i < Array.length l then + let hdx = l.(i) and hdy = l'.(i) in + let (n, eqT, restT) = destProd typ in + let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential dummy_loc env isevars eq in + let eq_app x = mkApp (Lazy.force eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) + in + aux (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in aux typ 0 (fun x -> x) + in (* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y); *) (* with _ -> ()); *) @@ -214,39 +230,14 @@ module Coercion = struct mkApp (prod.intro, [| a'; b'; x ; y |])) end else - (* if len = 1 && len = Array.length l' && i = i' then *) -(* let argx, argy = l.(0), l'.(0) in *) -(* let indtyp = Inductiveops.type_of_inductive env i in *) -(* let argname, argtype, _ = destProd indtyp in *) -(* let eq = *) -(* mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *) -(* in *) -(* let pred = mkLambda (argname, argtype, *) -(* mkApp (mkInd i, [| mkRel 1 |])) *) -(* in *) -(* let evar = make_existential dummy_loc env isevars eq in *) -(* Some (fun x -> *) -(* mkApp (Lazy.force eqrec, *) -(* [| argtype; argx; pred; x; argy; evar |])) *) -(* else *)subco () + if i = i' && len = Array.length l' then + Some (coerce_application (Typing.type_of env (evars_of !isevars) c) c c' l l') + else + subco () | x, y when x = y -> let lam_type = Typing.type_of env (evars_of !isevars) c in - let rec coerce typ i co = - if i < Array.length l then - let hdx = l.(i) and hdy = l'.(i) in - let (n, eqT, restT) = destProd typ in - let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in - let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in - let evar = make_existential dummy_loc env isevars eq in - let eq_app x = mkApp (Lazy.force eq_rect, - [| eqT; hdx; pred; x; hdy; evar|]) - in - coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) - else co - in if Array.length l = Array.length l' then ( - trace (str"Inserting coercion at application"); - Some (coerce lam_type 0 (fun x -> x)) + Some (coerce_application lam_type c c' l l') ) else subco () | _ -> subco ()) | _, _ -> subco () |