From 9ec08ac299faf6acdfd6061fd21a00e3446aec79 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 Sep 2014 15:03:34 +0200
Subject: Using an or_var rather than the hack with loc for coding a pure ident
 as a disjunctive intropattern.

---
 intf/tacexpr.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3501917f2b..2967c10dd7 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -44,9 +44,9 @@ type inversion_kind =
 
 type ('c,'id) inversion_strength =
   | NonDepInversion of
-      inversion_kind * 'id list * 'c or_and_intro_pattern_expr located option
+      inversion_kind * 'id list * 'c or_and_intro_pattern_expr located or_var option
   | DepInversion of
-      inversion_kind * 'c option * 'c or_and_intro_pattern_expr located option
+      inversion_kind * 'c option * 'c or_and_intro_pattern_expr located or_var option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -59,7 +59,7 @@ type 'id message_token =
 type 'constr induction_clause =
     'constr with_bindings induction_arg *
     (intro_pattern_naming_expr located option (* eqn:... *)
-    * 'constr or_and_intro_pattern_expr located option) (* as ... *)
+    * 'constr or_and_intro_pattern_expr located or_var option) (* as ... *)
 
 type ('constr,'id) induction_clause_list =
     'constr induction_clause list
-- 
cgit v1.2.3