From e40f33d24476a91fec447233efd2e921ff7c882b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Jun 2012 16:30:08 +0000
Subject: Fixing bug #2817 (occur check was not done up to instantiation of
 known instances in unification.ml). This refines the fix to bug #1918.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index e83be6d63b..d826fb605a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -235,6 +235,7 @@ val isVarId : identifier -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
+val isMetaOf : metavariable -> constr -> bool
 val isEvar_or_Meta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
-- 
cgit v1.2.3