From 8cf4e04fa817cf7ff9d73cb5cb7fff8b3b950387 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 18 Oct 2008 15:57:24 +0000
Subject: Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
 abusivement sur les clauses. Nettoyage au passage de metamap qui était
 utilisé à la fois pour les substitutions de meta et pour les contextes de
 typage de meta.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 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 2ab03e50fe..5d75df4bf2 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -208,6 +208,7 @@ type ('constr, 'types) kind_of_term =
    term *)
 
 val kind_of_term : constr -> (constr, types) kind_of_term
+val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term
 
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
-- 
cgit v1.2.3