From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- ltac/evar_tactics.ml | 2 +- ltac/rewrite.ml | 18 +++++++++--------- ltac/tacinterp.ml | 4 ++-- 3 files changed, 12 insertions(+), 12 deletions(-) (limited to 'ltac') diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index c5b26e6d56..5d3b2b886e 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -77,7 +77,7 @@ let let_evar name typ = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma typ in + let _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 076e4c05e4..5703687c48 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -113,7 +113,7 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in let evdref = ref evars in - let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in + let t = Typing.e_solve_evars env evdref (EConstr.of_constr (mkApp (fc, args))) in (!evdref, cstrs), t let app_poly_nocheck env evars f args = @@ -382,7 +382,7 @@ end let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in - let evd', t = Typing.type_of env (goalevars evars) c in + let evd', t = Typing.type_of env (goalevars evars) (EConstr.of_constr c) in (evd', cstrevars evars), c module PropGlobal = struct @@ -485,7 +485,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 = Typing.unsafe_type_of env evd (EConstr.of_constr argl) in let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) @@ -787,7 +787,7 @@ 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 appmtype = Typing.unsafe_type_of env (goalevars evars) (EConstr.of_constr appm) in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1477,7 +1477,7 @@ type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = let evdref = ref sigma in - let sort = Typing.e_sort_of env evdref concl in + let sort = Typing.e_sort_of env evdref (EConstr.of_constr concl) in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = @@ -1870,7 +1870,7 @@ let declare_projection n instance_id r = let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let term = proper_projection c ty in - let sigma, typ = Typing.type_of env sigma term in + let sigma, typ = Typing.type_of env sigma (EConstr.of_constr term) in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1902,7 +1902,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 = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in let cstrs = let rec aux t = match kind_of_term t with @@ -1932,7 +1932,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 = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2126,7 +2126,7 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let (sigma, t) = Typing.type_of env sigma rel in + let (sigma, t) = Typing.type_of env sigma (EConstr.of_constr rel) in let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 34faa028f2..8f5ac7e766 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let evdref = ref sigma in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref c in + let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in !evdref , c with | Not_found -> @@ -799,7 +799,7 @@ let interp_may_eval f ist env sigma = function (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) | ConstrTerm c -> try f ist env sigma c -- cgit v1.2.3