From d28c22a7b173fc78de98c8bf0f986cb163e210a0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Mar 2018 23:25:53 +0100 Subject: Make direct invocations of `simple apply` obey `Opaque` directive. When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues. --- pretyping/unification.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/unification.mli') diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 16ce5c93d..e2e261ae7 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr open Environ @@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : unit -> unify_flags +val default_no_delta_unify_flags : transparent_state -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags -- cgit v1.2.3