diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 137770d8f0..2f766afaa6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -38,7 +38,7 @@ let set_print_constr f = term_printer := f module EvMap = Evar.Map -let pr_evar_suggested_name evk sigma = +let evar_suggested_name evk sigma = let open Evd in let base_id evk' evi = match evar_ident evk' sigma with @@ -67,7 +67,7 @@ let pr_existential_key sigma evk = let open Evd in match evar_ident evk sigma with | None -> - str "?" ++ Id.print (pr_evar_suggested_name evk sigma) + str "?" ++ Id.print (evar_suggested_name evk sigma) | Some id -> str "?" ++ Id.print id @@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c = let open EConstr in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c + | Construct _ | Int _) -> c | Cast (b,k,t) -> let b' = f l b in let t' = f l t in @@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let open EConstr in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> cstr + | Construct _ | Int _) -> cstr | Cast (c,k, t) -> let c' = f l c in let t' = f l t in @@ -1417,11 +1417,9 @@ let prod_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l -(* Combinators on judgments *) - -let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } -let on_judgment_value f j = { j with uj_val = f j.uj_val } -let on_judgment_type f j = { j with uj_type = f j.uj_type } +let on_judgment = Environ.on_judgment +let on_judgment_value = Environ.on_judgment_value +let on_judgment_type = Environ.on_judgment_type (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in variables skips let-in's; let-in's in the middle are put in ctx2 *) |