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 +
 kernel/term.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'kernel')

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                 *)
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