diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 98d14f3d33..fbc64d95d0 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -289,18 +289,18 @@ end) = struct if Int.equal n 0 then c else match EConstr.kind sigma c with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> decomp_pointwise sigma (pred n) relb - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1])) | _ -> invalid_arg "decomp_pointwise" let rec apply_pointwise sigma rel = function | arg :: args -> (match EConstr.kind sigma rel with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> apply_pointwise sigma relb args - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args | _ -> invalid_arg "apply_pointwise") | [] -> rel @@ -357,7 +357,7 @@ end) = struct match EConstr.kind sigma t with | App (c, args) when Array.length args >= 2 -> let head = if isApp sigma c then fst (destApp sigma c) else c in - if Termops.is_global sigma (coq_eq_ref ()) head then None + if isRefX sigma (coq_eq_ref ()) head then None else (try let params, args = Array.chop (Array.length args - 2) args in @@ -483,7 +483,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.unsafe_type_of env evd argl in + let ty = Retyping.get_type_of env evd argl in let r = Retyping.relevance_of_type env evd ty in let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, @@ -789,7 +789,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in + let evd, appmtype = Typing.type_of env (goalevars evars) appm in + let evars = evd, snd evars in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1879,13 +1880,13 @@ let declare_projection n instance_id r = let rec aux t = match EConstr.kind sigma t with | App (f, [| a ; a' ; rel; rel' |]) - when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + when isRefX sigma (PropGlobal.respectful_ref ()) f -> succ (aux rel') | _ -> 0 in let init = match EConstr.kind sigma typ with - App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f -> mkApp (f, fst (Array.chop (Array.length args - 2) args)) | _ -> typ in aux init @@ -1906,7 +1907,7 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let cstrs = let rec aux t = match EConstr.kind sigma t with @@ -1936,7 +1937,7 @@ let build_morphism_signature env sigma m = let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2195,10 +2196,10 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - let open Tacmach.New in Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let ctype = pf_unsafe_type_of gl (mkVar id) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ctype = Retyping.get_type_of env sigma (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in let (equiv, args) = decompose_app sigma concl in let rec split_last_two = function |