diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 38 |
1 files changed, 6 insertions, 32 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 11a7f1941a..9c559e6cba 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -111,21 +111,10 @@ module Coercion = struct : (Term.constr -> Term.constr) option = let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in -(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *) -(* str " and "++ my_print_constr env y ++ *) -(* str " with evars: " ++ spc () ++ *) -(* my_print_evardefs !isevars); *) -(* with _ -> ()); *) let rec coerce_unify env x y = -(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y) *) -(* with _ -> ()); *) let x = hnf env isevars x and y = hnf env isevars y in try isevars := the_conv_x_leq env x y !isevars; - (* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) - (* str " and "++ my_print_constr env y); *) - (* with _ -> ()); *) None with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = @@ -133,10 +122,6 @@ module Coercion = struct let rec coerce_application typ typ' c c' l l' = let len = Array.length l in 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); *) -(* with _ -> ()); *) if i < len then let hdx = l.(i) and hdy = l'.(i) in try isevars := the_conv_x_leq env hdx hdy !isevars; @@ -165,10 +150,6 @@ module Coercion = struct 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 *) -(* ++ str "in env:" ++ my_print_env env); *) -(* with _ -> ()); *) match (kind_of_term x, kind_of_term y) with | Sort s, Sort s' -> (match s, s' with @@ -179,13 +160,6 @@ module Coercion = struct | Prod (name, a, b), Prod (name', a', b') -> let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in - -(* let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *) -(* let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *) -(* let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *) -(* let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *) -(* mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *) - let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt c1 (mkRel 1) in @@ -295,7 +269,6 @@ module Coercion = struct and subset_coerce env isevars x y = match disc_subset x with Some (u, p) -> - (* trace (str "Inserting projection "); *) let c = coerce_unify env u y in let f x = app_opt c (mkApp ((Lazy.force sig_).proj1, @@ -423,7 +396,11 @@ module Coercion = struct isevars, { uj_val = app_opt ct j.uj_val; uj_type = typ' } - + let inh_coerce_to_prod loc env isevars t = + let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in + let _, typ' = mu env isevars typ in + isevars, (fst t, typ') + 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 @@ -508,8 +485,7 @@ module Coercion = struct try let rels, rng = decompose_prod_n nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) - if noccur_with_meta 0 (succ nabsinit) rng then ( -(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) + if noccur_with_meta 0 (succ nabs) rng then ( let env', t, t' = let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in env', rng, lift nabs t' @@ -523,6 +499,4 @@ module Coercion = struct error_cannot_coerce env' sigma (t, t')) else isevars with _ -> isevars -(* trace (str "decompose_prod_n failed"); *) -(* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end |