From fd28f10096f82ef133bbf10512c8bee617b6b8b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 8 Oct 1999 08:18:57 +0000
Subject: deplacements des var. ex. hors du noyau

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index c36df1f65b..8622b8f3f9 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -15,6 +15,7 @@ type 'a oper =
   | Sort of 'a
   | Cast | Prod | Lambda
   | AppL | Const of section_path | Abst of section_path
+  | Evar of section_path
   | MutInd of section_path * int
   | MutConstruct of (section_path * int) * int
   | MutCase of case_info
@@ -75,13 +76,13 @@ type kindOfTerm =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsAppL         of constr array
-  | IsConst        of section_path  * constr array
-  | IsAbst         of section_path  * constr array
+  | IsConst        of section_path * constr array
+  | IsAbst         of section_path * constr array
+  | IsEvar         of section_path * constr array
   | IsMutInd       of section_path * int * constr array
   | IsMutConstruct of section_path * int * int * constr array
   | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of int array * int * constr array * name list *
-                      constr array
+  | IsFix          of int array * int * constr array * name list * constr array
   | IsCoFix        of int * constr array * name list * constr array
 
 (* Discriminates which kind of term is it.  
-- 
cgit v1.2.3