From 698c79dc28a13baf864c863800a2b48690207e34 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 10 Oct 2011 22:00:22 +0000
Subject: Applied the trick of Chung-Kil Hur to solve second-order matching
 problems with dependencies. Generalized it to matching over dependent tuples
 as explored by Dan Grayson. Currently used only in Evarconv.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/evarconv.mli')

diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index e1f507b0a..270d3f1e6 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -39,3 +39,5 @@ val check_conv_record : constr * types list -> constr * types list ->
     (constr list * types list) *
     (constr list * types list) * constr *
     (int * constr)
+
+val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
-- 
cgit v1.2.3