diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 53123c9334..a65b3941ef 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -770,6 +770,20 @@ let rec isArity sigma c = | Sort _ -> true | _ -> false +type arity = rel_context * ESorts.t + +let destArity sigma = + let open Context.Rel.Declaration in + let rec prodec_rec l c = + match kind sigma c with + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c + | Cast (c,_,_) -> prodec_rec l c + | Sort s -> l,s + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") + in + prodec_rec [] + let mkProd_or_LetIn decl c = let open Context.Rel.Declaration in match decl with @@ -817,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) +let map_rel_context_in_env f env sign = + let rec aux env acc = function + | d::sign -> + aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign + | [] -> + acc + in + aux env [] (List.rev sign) + let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, of_constr t |