diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 07fe902220..40b3d0d8b6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -288,6 +288,7 @@ let has_no_evar sigma = with Exit -> false let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) +let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l let pr_evar_universe_context ctx = let open UState in @@ -1462,6 +1463,18 @@ let prod_applist sigma c l = | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l +let prod_applist_assum sigma n c l = + let open EConstr in + let rec app n subst c l = + if Int.equal n 0 then + if l == [] then Vars.substl subst c + else anomaly (Pp.str "Not enough arguments.") + else match EConstr.kind sigma c, l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (Vars.substl subst b::subst) 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 } |