From a1be9ce30ed0c59d3cd8651ff0c624a24a6d3fc9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Sep 2014 09:50:07 +0200
Subject: Seeing IntroWildcard as an action intro pattern rather than as a
 naming pattern (the action is "clear").

Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.

Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
---
 intf/misctypes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index c61da0e306..2c8ac3a693 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -21,11 +21,11 @@ type 'constr intro_pattern_expr =
   | IntroNaming of intro_pattern_naming_expr
   | IntroAction of 'constr intro_pattern_action_expr
 and intro_pattern_naming_expr =
-  | IntroWildcard
   | IntroIdentifier of Id.t
   | IntroFresh of Id.t
   | IntroAnonymous
 and 'constr intro_pattern_action_expr =
+  | IntroWildcard
   | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
   | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
   | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
-- 
cgit v1.2.3