diff options
| author | Pierre-Marie Pédrot | 2016-02-15 13:31:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-15 13:41:16 +0100 |
| commit | 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 (patch) | |
| tree | 15aadd829fe3e8c3ee0a747de34a9b96614bfdba /tactics | |
| parent | 968dfdb15cc11d48783017b2a91147b25c854ad6 (diff) | |
Renaming functions in Typing to stick to the standard e_* scheme.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 |
4 files changed, 7 insertions, 7 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 97b5ba0cc5..30e157ffd3 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -74,7 +74,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.sort_of env sigma typ in + let _ = Typing.e_sort_of env sigma typ in let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c50535a17a..d0a090e5c1 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -107,7 +107,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.solve_evars env evdref (mkApp (fc, args)) in + let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in (!evdref, cstrs), t let app_poly_nocheck env evars f args = @@ -1452,7 +1452,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.sort_of env evdref concl in + let sort = Typing.e_sort_of env evdref concl in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1112da4a0d..91711c2f74 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -812,7 +812,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.solve_evars env evdref c in + let c = Typing.e_solve_evars env evdref c in !evdref , c with | Not_found -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 46e8798543..f76f4f6e20 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1814,7 +1814,7 @@ let check_is_type env ty msg = Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try - let _ = Typing.sort_of env evdref ty in + let _ = Typing.e_sort_of env evdref ty in Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> msg e @@ -1823,10 +1823,10 @@ let check_decl env (_, c, ty) msg = Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try - let _ = Typing.sort_of env evdref ty in + let _ = Typing.e_sort_of env evdref ty in let _ = match c with | None -> () - | Some c -> Typing.check env evdref c ty + | Some c -> Typing.e_check env evdref c ty in Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> |