From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- pretyping/evd.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/evd.mli') diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 5c508419..0b4f1853 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr * instance_status -> evar_map -> eva val clear_metas : evar_map -> evar_map (** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : evar_map -> evar_map -> evar_map +val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map -- cgit v1.2.3