From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Sep 2013 21:50:35 +0200
Subject: Adding generic solvers to term holes. For now, no resolution
 mechanism nor parsing is plugged.

---
 intf/constrexpr.mli | 2 +-
 intf/glob_term.mli  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 68a65c5c70..64bbd1e835 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -78,7 +78,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of Loc.t * Evar_kinds.t option
+  | CHole of Loc.t * Evar_kinds.t option * Genarg.raw_generic_argument option
   | CPatVar of Loc.t * (bool * patvar)
   | CEvar of Loc.t * existential_key * constr_expr list option
   | CSort of Loc.t * glob_sort
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 315b11517d..1d200ca79b 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -46,7 +46,7 @@ type glob_constr =
   | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array *
       glob_constr array * glob_constr array
   | GSort of Loc.t * glob_sort
-  | GHole of (Loc.t * Evar_kinds.t)
+  | GHole of (Loc.t * Evar_kinds.t * Genarg.glob_generic_argument option)
   | GCast of Loc.t * glob_constr * glob_constr cast_type
 
 and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
-- 
cgit v1.2.3