From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.

---
 pretyping/detyping.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/detyping.mli')

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cb478777f..97c636af7 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -60,6 +60,9 @@ val simple_cases_matrix_of_branches :
 val return_type_of_predicate :
   inductive -> int -> glob_constr -> predicate_pattern * glob_constr option
 
+val subst_genarg_hook :
+  (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
+
 module PrintingInductiveMake :
   functor (Test : sig
     val encode : Libnames.reference -> Names.inductive
-- 
cgit v1.2.3