modif lexer: ident peut commencer par _

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

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)