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.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index d274857af5..49d7afa22e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -261,6 +261,7 @@ let mkFix fix = Fix fix
 let mkCoFix cofix = CoFix cofix
 
 let kind_of_term c = c
+let kind_of_term2 c = c
 
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
-- 
cgit v1.2.3