diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index c3b82729d5..864b1a625c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -295,6 +295,6 @@ val whd_betaiota_deltazeta_for_iota_state : state * Cst_stack.t (** {6 Meta-related reduction functions } *) -val meta_instance : evar_map -> constr freelisted -> constr +val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr val nf_meta : evar_map -> constr -> constr -val meta_reducible_instance : evar_map -> constr freelisted -> constr +val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr |