From 9d7499dcd4440aca458cb190ed108ae9b3adff17 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 18 Jun 2011 20:35:22 +0000 Subject: Generalizing flag use_evars_pattern_unification into a flag use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping/unification.mli') diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 44b1c3889..37eaa5802 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -12,11 +12,12 @@ open Evd type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; - use_metas_eagerly : bool; + use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; resolve_evars : bool; - use_evars_pattern_unification : bool; + use_pattern_unification : bool; + use_meta_bound_pattern_unification : bool; frozen_evars : ExistentialSet.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; -- cgit v1.2.3