From 801b4eea7475660813dac697d375a5847af3e7b3 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 25 Nov 2003 17:19:44 +0000
Subject: modif lexer: ident peut commencer par _

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c5b2989552..ce1e36e032 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -309,6 +309,12 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (substl make_abs) lc
 
+(* [env] is the typing environment
+   [n] is the dB of the last inductive type
+   [ntypes] is the number of inductive types in the definition
+     (i.e. range of inductives is [n; n+ntypes-1])
+   [lra] is the list of recursive tree of each variable
+ *) 
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
  (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
 
-- 
cgit v1.2.3