diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 01:07:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:56 +0100 |
| commit | db252cb87e9c63f400fd4fddd2d771df3160d592 (patch) | |
| tree | 25c1cb44c479ffa10e6db87f91b43f7e60b427bd /pretyping/reductionops.mli | |
| parent | 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 (diff) | |
Inv API using EConstr.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 864b1a625..e67fad3fd 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -213,9 +213,9 @@ val hnf_lam_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr val hnf_lam_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr val hnf_lam_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr -val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr -val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * constr) list * sorts +val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr +val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr +val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts val sort_of_arity : env -> evar_map -> EConstr.t -> sorts val splay_prod_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr val splay_lam_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr |