From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 19 May 2008 20:58:36 +0000 (+0000)
Subject: added leftno to references f inductive types and constructors, more unifor names... 
X-Git-Tag: make_still_working~5145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4d71b463ae8510e80a40cf4df475d19fab3df2c;p=helm.git

added leftno to references f inductive types and constructors, more unifor names of modules, NCic -> C and NReference Ref everywhere
---

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index e67e1ba90..20482ec71 100644
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -35,14 +35,14 @@ let convert_term uri n_fl t =
  | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp 
  | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
  | NCic.Implicit _ -> assert false
- | NCic.Const (NReference.Ref (u,NReference.Ind (_,i))) -> 
+ | NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) -> 
      Cic.MutInd (ouri_of_nuri u,i,[])
- | NCic.Const (NReference.Ref (u,NReference.Con (i,j))) -> 
+ | NCic.Const (NReference.Ref (u,NReference.Con (i,j,_))) -> 
      Cic.MutConstruct (ouri_of_nuri u,i,j,[])
  | NCic.Const (NReference.Ref (u,NReference.Def _))
  | NCic.Const (NReference.Ref (u,NReference.Decl)) ->
      Cic.Const (ouri_of_nuri u,[])
- | NCic.Match (NReference.Ref (u,NReference.Ind (_,i)),oty,t,pl) ->
+ | NCic.Match (NReference.Ref (u,NReference.Ind (_,i,_)),oty,t,pl) ->
      Cic.MutCase (ouri_of_nuri u,i, convert_term k oty, convert_term k t,
        List.map (convert_term k) pl)
  | NCic.Const (NReference.Ref (u,NReference.Fix (i,_,_))) 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index de785bde8..bd0587a43 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -11,6 +11,9 @@
 
 (* $Id$ *)
 
+module C = NCic
+module Ref = NReference
+
 exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
@@ -118,69 +121,60 @@ let get_checked_obj u =
 ;;
 
 let get_checked_decl = function
-  | NReference.Ref (uri, NReference.Decl) ->
+  | Ref.Ref (uri, Ref.Decl) ->
       (match get_checked_obj uri with
-      | _,height,_,_, NCic.Constant (rlv,name,None,ty,att) ->
+      | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
           rlv,name,ty,att,height
-      | _,_,_,_, NCic.Constant (_,_,Some _,_,_) ->
+      | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
           prerr_endline "get_checked_decl on a definition"; assert false
       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
 ;;
 
 let get_checked_def = function
-  | NReference.Ref (uri, NReference.Def _) ->
+  | Ref.Ref (uri, Ref.Def _) ->
       (match get_checked_obj uri with
-      | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
+      | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
           rlv,name,bo,ty,att,height
-      | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
+      | _,_,_,_, C.Constant (_,_,None,_,_) ->
           prerr_endline "get_checked_def on an axiom"; assert false
       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
   | _ -> prerr_endline "get_checked_def on a non def"; assert false
 ;;
 
 let get_checked_indtys = function
-  | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
+  | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
       (match get_checked_obj uri with
-      | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
+      | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
         inductive,leftno,tys,att,n
       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 ;;
 
 let get_checked_fixes_or_cofixes = function
-  | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))->
+  | Ref.Ref (uri, (Ref.Fix (fixno,_,_)|Ref.CoFix fixno))->
       (match get_checked_obj uri with
-      | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
+      | _,height,_,_, C.Fixpoint (_,funcs,att) ->
          funcs, att, height
       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
-  | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
-;;
-
-let get_indty_leftno = function 
-  | NReference.Ref (uri, NReference.Ind _) 
-  | NReference.Ref (uri, NReference.Con _) ->
-      (match get_checked_obj uri with
-      | _,_,_,_, NCic.Inductive (_,left,_,_) -> left
-      | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
-  | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
+  | r -> prerr_endline ("get_checked_(co)fix on " ^ Ref.string_of_reference r); assert false
 ;;
 
-let get_relevance (NReference.Ref (_, infos) as r) =
+let get_relevance (Ref.Ref (_, infos) as r) =
   match infos with
-     NReference.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
-   | NReference.Decl -> let res,_,_,_,_ = get_checked_decl r in res
-   | NReference.Ind _ ->
+     Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
+   | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
+   | Ref.Ind _ ->
        let _,_,tl,_,n = get_checked_indtys r in
        let res,_,_,_ = List.nth tl n in
          res
-    | NReference.Con (_,i) ->
+    | Ref.Con (_,i,_) ->
        let _,_,tl,_,n = get_checked_indtys r in
        let _,_,_,cl = List.nth tl n in
        let res,_,_ = List.nth cl (i - 1) in
          res
-    | NReference.Fix (fixno,_,_)
-    | NReference.CoFix fixno ->
+    | Ref.Fix (fixno,_,_)
+    | Ref.CoFix fixno ->
         let fl,_,_ = get_checked_fixes_or_cofixes r in
         let res,_,_,_,_ = List.nth fl fixno in
           res
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 272530a1a..67b3857d1 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -43,8 +43,6 @@ val get_checked_fixes_or_cofixes:
   NReference.reference -> 
    NCic.inductiveFun list * NCic.f_attr * int
 
-val get_indty_leftno: NReference.reference -> int
-
 val invalidate: unit -> unit
 
 val set_typecheck_obj: (NCic.obj -> unit) -> unit
diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 8ae842868..449c4313b 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -27,12 +27,12 @@ module R = NReference
 let r2s pp_fix_name r = 
   try
     match r with
-    | R.Ref (u,R.Ind (_,i)) -> 
+    | R.Ref (u,R.Ind (_,i,_)) -> 
         (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,name,_,_ = List.nth itl i in name
         | _ -> assert false)
-    | R.Ref (u,R.Con (i,j)) -> 
+    | R.Ref (u,R.Con (i,j,_)) -> 
         (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,_,_,cl = List.nth itl i in
diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index b71fb499a..73f78dc36 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -11,46 +11,38 @@
 
 (* $Id$ *)
 
-(* TODO unify exceptions *)
+module C = NCic
+module Ref = NReference
 
-module type Strategy =
- sig
+module type Strategy = sig
   type stack_term
   type env_term
-  type config = int * env_term list * NCic.term * stack_term list
+  type config = int * env_term list * C.term * stack_term list
   val to_env :
-   reduce: (config -> config) ->
-   unwind: (config -> NCic.term) ->
-   config -> env_term
+   reduce: (config -> config) -> unwind: (config -> C.term) ->
+    config -> env_term
   val from_stack : stack_term -> config
   val from_stack_list_for_unwind :
-   unwind: (config -> NCic.term) ->
-   stack_term list -> NCic.term list
+   unwind: (config -> C.term) -> stack_term list -> C.term list
   val from_env : env_term -> config
   val from_env_for_unwind :
-   unwind: (config -> NCic.term) ->
-   env_term -> NCic.term
+   unwind: (config -> C.term) -> env_term -> C.term
   val stack_to_env :
-   reduce: (config -> config) ->
-   unwind: (config -> NCic.term) ->
-   stack_term -> env_term
+   reduce: (config -> config) -> unwind: (config -> C.term) ->
+    stack_term -> env_term
   val compute_to_env :
-   reduce: (config -> config) ->
-   unwind: (config -> NCic.term) ->
-   int -> env_term list -> 
-    NCic.term -> env_term
+   reduce: (config -> config) -> unwind: (config -> C.term) ->
+    int -> env_term list -> C.term -> env_term
   val compute_to_stack :
-   reduce: (config -> config) ->
-   unwind: (config -> NCic.term) ->
-   config -> stack_term
+   reduce: (config -> config) -> unwind: (config -> C.term) ->
+    config -> stack_term
  end
 ;;
 
-module CallByValueByNameForUnwind' =
- struct
-  type config = int * env_term list * NCic.term * stack_term list
-  and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
-  and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
+module CallByValueByNameForUnwind' = struct
+  type config = int * env_term list * C.term * stack_term list
+  and stack_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
+  and env_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
   let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
   let from_stack (c,_) = Lazy.force c
   let from_stack_list_for_unwind ~unwind:_ l = 
@@ -65,286 +57,10 @@ module CallByValueByNameForUnwind' =
  end
 ;;
 
-
-(* {{{ module CallByValueByNameForUnwind =
- struct
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  and stack_term = config
-  and env_term = config * config (* cbv, cbn *)
-  and ens_term = config * config (* cbv, cbn *)
-
-  let to_env c = c,c
-  let to_ens c = c,c
-  let from_stack config = config
-  let from_stack_list_for_unwind ~unwind l = List.map unwind l
-  let from_env (c,_) = c
-  let from_ens (c,_) = c
-  let from_env_for_unwind ~unwind (_,c) = unwind c
-  let from_ens_for_unwind ~unwind (_,c) = unwind c
-  let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
-  let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
-  let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-
-(* Old Machine *)
-module CallByNameStrategy =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let from_env_for_unwind ~unwind v = v
-  let from_ens_for_unwind ~unwind v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
-  let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
- end
-;;
-
-module CallByNameStrategy =
- struct
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  and stack_term = config
-  and env_term = config
-  and ens_term = config
-
-  let to_env c = c
-  let to_ens c = c
-  let from_stack config = config
-  let from_stack_list_for_unwind ~unwind l = List.map unwind l
-  let from_env c = c
-  let from_ens c = c
-  let from_env_for_unwind ~unwind c = unwind c
-  let from_ens_for_unwind ~unwind c = unwind c
-  let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
-  let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
-  let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-module CallByValueStrategy =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let from_env_for_unwind ~unwind v = v
-  let from_ens_for_unwind ~unwind v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- end
-;;
-
-module CallByValueStrategyByNameOnConstants =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let from_env_for_unwind ~unwind v = v
-  let from_ens_for_unwind ~unwind v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens =
-   function
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens =
-   function
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
- end
-;;
-
-module LazyCallByValueStrategy =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let from_env_for_unwind ~unwind v = Lazy.force v
-  let from_ens_for_unwind ~unwind v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
-  let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByValueStrategyByNameOnConstants =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let from_env_for_unwind ~unwind v = Lazy.force v
-  let from_ens_for_unwind ~unwind v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t =
-   lazy (
-    match t with
-       Cic.Const _ as t -> unwind k e ens t    
-     | t -> reduce (k,e,ens,t,[]))
-  let compute_to_env ~reduce ~unwind k e ens t =
-   lazy (
-    match t with
-       Cic.Const _ as t -> unwind k e ens t    
-     | t -> reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByNameStrategy =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let from_env_for_unwind ~unwind v = Lazy.force v
-  let from_ens_for_unwind ~unwind v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
-  let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- end
-;;
-
-module
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
-=
- struct
-  type stack_term = reduce:bool -> Cic.term
-  type env_term = reduce:bool -> Cic.term
-  type ens_term = reduce:bool -> Cic.term
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let to_ens v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let from_stack ~unwind v = (v ~reduce:false)
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = (v ~reduce:true)
-  let from_ens v = (v ~reduce:true)
-  let from_env_for_unwind ~unwind v = (v ~reduce:true)
-  let from_ens_for_unwind ~unwind v = (v ~reduce:true)
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t =
-   let svalue =
-     lazy (
-      match t with
-         Cic.Const _ as t -> unwind k e ens t    
-       | t -> reduce (k,e,ens,t,[])
-     ) in
-   let lvalue =
-    lazy (unwind k e ens t)
-   in
-    fun ~reduce ->
-     if reduce then Lazy.force svalue else Lazy.force lvalue
-  let compute_to_env ~reduce ~unwind k e ens t =
-   let svalue =
-     lazy (
-      match t with
-         Cic.Const _ as t -> unwind k e ens t    
-       | t -> reduce (k,e,ens,t,[])
-     ) in
-   let lvalue =
-    lazy (unwind k e ens t)
-   in
-    fun ~reduce ->
-     if reduce then Lazy.force svalue else Lazy.force lvalue
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsStrategy =
- struct
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  and stack_term = config
-  and env_term = config
-  and ens_term = config
-
-  let to_env config = config
-  let to_ens config = config
-  let from_stack config = config
-  let from_stack_list_for_unwind ~unwind l = List.map unwind l
-  let from_env v = v
-  let from_ens v = v
-  let from_env_for_unwind ~unwind config = unwind config
-  let from_ens_for_unwind ~unwind config = unwind config
-  let stack_to_env ~reduce ~unwind config = reduce config
-  let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
-  let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
- struct
-  type stack_term =
-   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = v
-  let from_ens v = v
-  let from_env_for_unwind ~unwind v = v
-  let from_ens_for_unwind ~unwind v = v
-  let stack_to_env ~reduce ~unwind (k,e,ens,t) =
-   match t with
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t =
-   unwind k e ens t
-  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-}}} *)
-
-module Reduction(RS : Strategy) =
- struct
+module Reduction(RS : Strategy) = struct
   type env = RS.env_term list
   type stack = RS.stack_term list
-  type config = int * env * NCic.term * stack
+  type config = int * env * C.term * stack
 
   let rec unwind (k,e,t,s) =
     let t = 
@@ -354,7 +70,7 @@ module Reduction(RS : Strategy) =
           (RS.from_env_for_unwind ~unwind) e t
     in
     if s = [] then t 
-    else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
+    else C.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
   ;;
 
   let list_nth l n = try List.nth l n with Failure _ -> assert false;;
@@ -367,43 +83,43 @@ module Reduction(RS : Strategy) =
 
   let rec reduce ~delta ?(subst = []) context : config -> config = 
    let rec aux = function
-     | k, e, NCic.Rel n, s when n <= k ->
+     | k, e, C.Rel n, s when n <= k ->
         let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
         aux (k',e',t',s'@s)
-     | k, _, NCic.Rel n, s as config (* when n > k *) ->
+     | k, _, C.Rel n, s as config (* when n > k *) ->
         let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
          (match x with
-         | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
+         | Some(_,C.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
          | _ -> config)
-     | (k, e, NCic.Meta (n,l), s) as config ->
+     | (k, e, C.Meta (n,l), s) as config ->
         (try 
            let _,_, term,_ = NCicUtils.lookup_subst n subst in
            aux (k, e, NCicSubstitution.subst_meta l term,s)
          with  NCicUtils.Subst_not_found _ -> config)
-     | (_, _, NCic.Implicit _, _) -> assert false
-     | (_, _, NCic.Sort _, _)
-     | (_, _, NCic.Prod _, _)
-     | (_, _, NCic.Lambda _, []) as config -> config
-     | (k, e, NCic.Lambda (_,_,t), p::s) ->
+     | (_, _, C.Implicit _, _) -> assert false
+     | (_, _, C.Sort _, _)
+     | (_, _, C.Prod _, _)
+     | (_, _, C.Lambda _, []) as config -> config
+     | (k, e, C.Lambda (_,_,t), p::s) ->
          aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
-     | (k, e, NCic.LetIn (_,_,m,t), s) ->
+     | (k, e, C.LetIn (_,_,m,t), s) ->
         let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
          aux (k+1, m'::e, t, s)
-     | (_, _, NCic.Appl [], _) -> assert false
-     | (k, e, NCic.Appl (he::tl), s) ->
+     | (_, _, C.Appl ([]|[_]), _) -> assert false
+     | (k, e, C.Appl (he::tl), s) ->
         let tl' =
          List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
         in
          aux (k, e, he, tl' @ s)
-     | (_, _, NCic.Const
-            (NReference.Ref (_,NReference.Def height) as refer), s) as config ->
+     | (_, _, C.Const
+            (Ref.Ref (_,Ref.Def height) as refer), s) as config ->
          if delta >= height then config else 
            let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
            aux (0, [], body, s) 
-     | (_, _, NCic.Const (NReference.Ref (_,
-            (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
-     | (_, _, NCic.Const (NReference.Ref 
-           (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config ->
+     | (_, _, C.Const (Ref.Ref (_,
+            (Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config -> config
+     | (_, _, C.Const (Ref.Ref 
+           (_,Ref.Fix (fixno,recindex,height)) as refer),s) as config ->
         if delta >= height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -413,28 +129,26 @@ module Reduction(RS : Strategy) =
         | Some recparam ->
            let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
            match reduce ~delta:0 ~subst context recparam with
-           | (_,_,NCic.Const (NReference.Ref (_,NReference.Con _)), _) as c ->
+           | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
                let new_s =
                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
                in
                let _,_,_,_,body = List.nth fixes fixno in
                aux (0, [], body, new_s)
            | _ -> config)
-     | (k, e, NCic.Match (_,_,term,pl),s) as config ->
+     | (k, e, C.Match (_,_,term,pl),s) as config ->
         let decofix = function
-          | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)->
+          | (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)->
              let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
              let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config
         in
         (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
-        | (_, _, NCic.Const (NReference.Ref (_,NReference.Con (_,j))),[]) ->
+        | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
             aux (k, e, List.nth pl (j-1), s)
-        | (_, _, NCic.Const 
-             (NReference.Ref (_,NReference.Con (_,j)) as refer), s') ->
-          let leftno = NCicEnvironment.get_indty_leftno refer in
-          let _,params = HExtlib.split_nth leftno s' in
+        | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')->
+          let _,params = HExtlib.split_nth lno s' in
           aux (k, e, List.nth pl (j-1), params@s)
         | _ -> config)
    in
@@ -449,44 +163,13 @@ module Reduction(RS : Strategy) =
 ;;
 
 
-(* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
-           senza ridurre la testa
-module R = Reduction CallByNameStrategy;; OK 56.368s
-module R = Reduction CallByValueStrategy;; ROTTO
-module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
-module R = Reduction LazyCallByValueStrategy;; ROTTO
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
-module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
-module R = Reduction
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
- OK 59.058s
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
-module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
-module R = Reduction(CallByValueByNameForUnwind);; 
-module R = Reduction(CallByNameStrategy);;
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
 module RS = CallByValueByNameForUnwind';;
-
 module R = Reduction(RS);;
-module U = UriManager;;
 
 let whd = R.whd
 
-(*
-let whd =
- let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
-  fun ?(delta=true) ?(subst=[]) context t ->
-   profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
-*)
-
-(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
- * fallbacks to structural equality *)
 let (===) x y = Pervasives.compare x y = 0 ;;
 
-module C = NCic
-
 (* t1, t2 must be well-typed *)
 let are_convertible whd ?(subst=[])  =
  let rec aux test_eq_only context t1 t2 =
@@ -553,7 +236,7 @@ let are_convertible whd ?(subst=[])  =
 
        | (C.Match (ref1,outtype1,term1,pl1),
           C.Match (ref2,outtype2,term2,pl2)) -> 
-           NReference.eq ref1 ref2 &&
+           Ref.eq ref1 ref2 &&
            aux test_eq_only context outtype1 outtype2 &&
            aux test_eq_only context term1 term2 &&
            (try List.for_all2 (aux test_eq_only context) pl1 pl2
@@ -566,10 +249,10 @@ let are_convertible whd ?(subst=[])  =
      true
    else
      let height_of = function
-      | NCic.Const (NReference.Ref (_,NReference.Def h)) 
-      | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h))) 
-      | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_) 
-      | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
+      | C.Const (Ref.Ref (_,Ref.Def h)) 
+      | C.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
+      | C.Appl(C.Const(Ref.Ref(_,Ref.Def h))::_) 
+      | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
       | _ -> 0
      in
      let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
@@ -616,7 +299,7 @@ let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
   | _, C.Lambda(_,_,bo), arg::tl ->
      let bo = NCicSubstitution.subst arg bo in
      head_beta_reduce ~delta ~upto:(upto - 1) bo tl
-  | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _ 
+  | _, C.Const (Ref.Ref (_, Ref.Def height) as re), _ 
     when delta <= height ->
       let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
       head_beta_reduce ~upto ~delta bo l
diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 11d17de32..6c5bb4a9a 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -11,18 +11,21 @@
 
 (* $Id$ *)
 
+module C = NCic 
+module Ref = NReference
+
 let debug_print = fun _ -> ();;
 
 let lift_from k n =
  let rec liftaux k = function
-    | NCic.Rel m as t -> if m < k then t else NCic.Rel (m + n)
-    | NCic.Meta (i,(m,l)) as t when k <= m ->
-       if n = 0 then t else NCic.Meta (i,(m+n,l))
-    | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
-    | NCic.Meta (i,(m,l)) -> 
+    | C.Rel m as t -> if m < k then t else C.Rel (m + n)
+    | C.Meta (i,(m,l)) as t when k <= m ->
+       if n = 0 then t else C.Meta (i,(m+n,l))
+    | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
+    | C.Meta (i,(m,l)) -> 
        let lctx = NCicUtils.expand_local_context l in
-       NCic.Meta (i, (m, NCic.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
-    | NCic.Implicit _ -> (* was the identity *) assert false
+       C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
+    | C.Implicit _ -> (* was the identity *) assert false
     | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t
  in
  liftaux k
@@ -43,37 +46,37 @@ let lift ?(from=1) n t =
 let rec psubst ?(avoid_beta_redexes=false) map_arg args = 
  let nargs = List.length args in
  let rec substaux k = function
-   | NCic.Rel n as t ->
+   | C.Rel n as t ->
       (match n with
       | n when n >= (k+nargs) ->
-         if nargs <> 0 then NCic.Rel (n - nargs) else t
+         if nargs <> 0 then C.Rel (n - nargs) else t
       | n when n < k -> t
       | n (* k <= n < k+nargs *) ->
        (try lift (k-1) (map_arg (List.nth args (n-k)))
         with Failure _ -> assert false))
-   | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
-       if nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
-   | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> 
-       if nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
-   | NCic.Meta (i,(m,l)) -> 
+   | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
+       if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
+   | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m -> 
+       if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+   | C.Meta (i,(m,l)) -> 
       let lctx = NCicUtils.expand_local_context l in
       (* 1-nargs < k-m, when <= 0 is still reasonable because we will
        * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
-      NCic.Meta (i,(m, NCic.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
-   | NCic.Implicit _ -> assert false (* was identity *)
-   | NCic.Appl (he::tl) as t ->
+      C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+   | C.Implicit _ -> assert false (* was identity *)
+   | C.Appl (he::tl) as t ->
       (* Invariant: no Appl applied to another Appl *)
       let rec avoid he' = function
         | [] -> he'
         | arg::tl' as args->
             (match he' with
-            | NCic.Appl l -> NCic.Appl (l@args)
-            | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
+            | C.Appl l -> C.Appl (l@args)
+            | C.Lambda (_,_,bo) when avoid_beta_redexes ->
                 (* map_arg is here \x.x, Obj magic is needed because 
                  * we don't have polymorphic recursion w/o records *)
                 avoid (psubst 
                   ~avoid_beta_redexes Obj.magic [Obj.magic arg] bo) tl'
-            | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args))
+            | _ -> if he == he' && args == tl then t else C.Appl (he'::args))
       in
       let tl = HExtlib.sharing_map (substaux k) tl in
       avoid (substaux k he) tl
@@ -90,7 +93,7 @@ let subst ?avoid_beta_redexes arg =
 (*  [t_i] is lifted as usual when it crosses an abstraction                  *)
 (* subst_meta (n, Non) t -> lift n t                                         *)
 let subst_meta = function 
-  | m, NCic.Irl _ 
-  | m, NCic.Ctx [] -> lift m 
-  | m, NCic.Ctx l  -> psubst (lift m) l 
+  | m, C.Irl _ 
+  | m, C.Ctx [] -> lift m 
+  | m, C.Ctx l  -> psubst (lift m) l 
 ;;
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index bd660903c..ae145a9c6 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -12,8 +12,8 @@
 (* $Id$ *)
 
 module C = NCic 
-module R = NCicReduction
 module Ref = NReference
+module R = NCicReduction
 module S = NCicSubstitution 
 module U = NCicUtils
 module E = NCicEnvironment
@@ -22,10 +22,12 @@ module PP = NCicPp
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
+(*
 let raise = function
   | TypeCheckerFailure s as e -> prerr_endline (Lazy.force s); raise e
   | e -> raise e
 ;;
+*)
 
 type recf_entry = 
   | Evil of int (* rno *) 
@@ -112,7 +114,7 @@ let debruijn uri number_of_types context =
       if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
    | C.Meta _ -> t
    | C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no))) 
-   | C.Const (Ref.Ref (uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
+   | C.Const (Ref.Ref (uri1,Ref.Ind (_,no,_))) when NUri.eq uri uri1 ->
       C.Rel (k + number_of_types - no)
    | t -> U.map (fun _ k -> k+1) k aux t
  in
@@ -189,8 +191,8 @@ let rec instantiate_parameters params c =
 
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
-  | C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref)  
-  | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
+  | C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref)  
+  | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref) :: _ ) as ty ->
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
@@ -205,7 +207,7 @@ let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term =
   let len = List.length context in
   let context_dcl = 
     match E.get_checked_obj r_uri with
-    | _,_,_,_, NCic.Inductive (_,_,tys,_) -> 
+    | _,_,_,_, C.Inductive (_,_,tys,_) -> 
         context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys
     | _ -> assert false
   in
@@ -275,8 +277,8 @@ let rec weakly_positive ~subst context n nn uri te =
   let dummy = C.Sort C.Prop in
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
-    | C.Const (Ref.Ref (uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0))))::tl) 
+    | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::tl) 
         when NUri.eq uri' uri -> dummy
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
@@ -308,7 +310,7 @@ and strictly_positive ~subst context n nn te =
        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.for_all (does_not_occur ~subst context n nn) tl
-   | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as r)::tl) -> 
+   | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
       let ok = List.length tyl = 1 in
@@ -446,7 +448,7 @@ let rec typeof ~subst ~metasenv context term =
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
       let constructorsno =
@@ -859,7 +861,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
          ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
-  | C.Match (Ref.Ref (uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
+  | C.Match (Ref.Ref (uri,Ref.Ind (true,_,_)),outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
          let ty = typeof ~subst ~metasenv context term in
@@ -901,8 +903,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h && List.for_all (does_not_occur ~subst context n nn) tl
    | C.Const (Ref.Ref (_,Ref.Con _)) -> true
-   | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j)) as ref) :: tl) as t ->
-      let _, paramsno, _, _, _ = E.get_checked_indtys ref in
+   | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j,paramsno))) :: tl) as t ->
       let ty_t = typeof ~subst ~metasenv context t in
       let dc_ctx, dcl, start, stop = 
         specialize_and_abstract_constrs ~subst indURI indlen context ty_t in
@@ -981,7 +982,7 @@ and is_really_smaller
  | C.Appl [] 
  | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
  | C.Meta _ -> true 
- | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_)),outtype,term,pl) ->
+ | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_,_)),outtype,term,pl) ->
     (match term with
     | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
         if not isinductive then
@@ -1001,8 +1002,8 @@ and is_really_smaller
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
-  | C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref) 
-  | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)::_) ->
+  | C.Const (Ref.Ref (uri,Ref.Ind (false,_,_)) as ref) 
+  | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_,_)) as ref)::_) ->
      let _, _, itl, _, _ = E.get_checked_indtys ref in
      Some (uri,List.length itl)
   | C.Prod (n,so,de) ->
@@ -1014,10 +1015,12 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
   raise (TypeCheckerFailure (lazy "Inconsistent cached infos in reference"))
  in
   match E.get_checked_obj uri, ref with
-  | (_,_,_,_,C.Inductive (isind1,_,tl,_)), Ref.Ref (_,Ref.Ind (isind2,i))  ->
+  | (_,_,_,_,C.Inductive(isind1,lno1,tl,_)),Ref.Ref(_,Ref.Ind (isind2,i,lno2))->
       if isind1 <> isind2 then error ();
+      if lno1 <> lno2 then error ();
       let _,_,arity,_ = List.nth tl i in arity
-  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j))  ->
+  | (_,_,_,_,C.Inductive (_,lno1,tl,_)), Ref.Ref (_,Ref.Con (i,j,lno2))  ->
+      if lno1 <> lno2 then error ();
       let _,_,_,cl = List.nth tl i in 
       let _,_,arity = List.nth cl (j-1) in 
       arity
@@ -1050,8 +1053,7 @@ let typecheck_context ~metasenv ~subst context =
             "the type of the definiens for %s in the context is not "^^
             "convertible with the declared one.\n"^^
             "inferred type:\n%s\nexpected type:\n%s")
-            name
-            (PP.ppterm ~subst ~metasenv ~context ty') 
+            name (PP.ppterm ~subst ~metasenv ~context ty') 
             (PP.ppterm ~subst ~metasenv ~context ty))))
      end;
      d::context
diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml
index 3d3c2d90e..f4f77a367 100644
--- a/helm/software/components/ng_kernel/nCicUtils.ml
+++ b/helm/software/components/ng_kernel/nCicUtils.ml
@@ -11,17 +11,20 @@
 
 (* $Id$ *)
 
+module C = NCic
+module Ref = NReference
+
 exception Subst_not_found of int
 exception Meta_not_found of int
 
 let expand_local_context = function
-  | NCic.Irl len -> 
+  | C.Irl len -> 
       let rec aux acc = function 
         | 0 -> acc
-        | n -> aux (NCic.Rel n::acc) (n-1)
+        | n -> aux (C.Rel n::acc) (n-1)
       in
        aux [] len
-  | NCic.Ctx lctx -> lctx
+  | C.Ctx lctx -> lctx
 ;;
 
 let lookup_subst n subst =
@@ -37,43 +40,43 @@ let lookup_meta n metasenv =
 ;;
 
 let fold g k f acc = function
- | NCic.Meta _ -> assert false
- | NCic.Implicit _
- | NCic.Sort _
- | NCic.Const _
- | NCic.Rel _ -> acc
- | NCic.Appl [] | NCic.Appl [_] -> assert false
- | NCic.Appl l -> List.fold_left (f k) acc l
- | NCic.Prod (n,s,t)
- | NCic.Lambda (n,s,t) -> f (g (n,NCic.Decl s) k) (f k acc s) t
- | NCic.LetIn (n,ty,t,bo) -> f (g (n,NCic.Def (t,ty)) k) (f k (f k acc ty) t) bo
- | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
+ | C.Meta _ -> assert false
+ | C.Implicit _
+ | C.Sort _
+ | C.Const _
+ | C.Rel _ -> acc
+ | C.Appl [] | C.Appl [_] -> assert false
+ | C.Appl l -> List.fold_left (f k) acc l
+ | C.Prod (n,s,t)
+ | C.Lambda (n,s,t) -> f (g (n,C.Decl s) k) (f k acc s) t
+ | C.LetIn (n,ty,t,bo) -> f (g (n,C.Def (t,ty)) k) (f k (f k acc ty) t) bo
+ | C.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
 ;;
 
 let map g k f = function
- | NCic.Meta _ -> assert false
- | NCic.Implicit _
- | NCic.Sort _
- | NCic.Const _
- | NCic.Rel _ as t -> t
- | NCic.Appl [] | NCic.Appl [_] -> assert false
- | NCic.Appl l as orig ->
+ | C.Meta _ -> assert false
+ | C.Implicit _
+ | C.Sort _
+ | C.Const _
+ | C.Rel _ as t -> t
+ | C.Appl [] | C.Appl [_] -> assert false
+ | C.Appl l as orig ->
     (match HExtlib.sharing_map (f k) l with
-      | NCic.Appl l :: tl -> NCic.Appl (l@tl)
+      | C.Appl l :: tl -> C.Appl (l@tl)
       | l1 when l == l1 -> orig
-      | l1 -> NCic.Appl l1)
- | NCic.Prod (n,s,t) as orig ->
-     let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
-     if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
- | NCic.Lambda (n,s,t) as orig -> 
-     let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
-     if t1 == t && s1 == s then orig else NCic.Lambda (n,s1,t1)
- | NCic.LetIn (n,ty,t,b) as orig -> 
+      | l1 -> C.Appl l1)
+ | C.Prod (n,s,t) as orig ->
+     let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+     if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
+ | C.Lambda (n,s,t) as orig -> 
+     let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+     if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
+ | C.LetIn (n,ty,t,b) as orig -> 
      let ty1 = f k ty in let t1 = f k t in
-     let b1 = f (g (n,NCic.Def (t,ty)) k) b in
-     if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1)
- | NCic.Match (r,oty,t,pl) as orig -> 
+     let b1 = f (g (n,C.Def (t,ty)) k) b in
+     if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
+ | C.Match (r,oty,t,pl) as orig -> 
      let oty1 = f k oty in let t1 = f k t in let pl1 = HExtlib.sharing_map (f k) pl in
      if oty1 == oty && t1 == t && pl1 == pl then orig 
-     else NCic.Match(r,oty1,t1,pl1)
+     else C.Match(r,oty1,t1,pl1)
 ;;
diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml
index 1b2c0cc2b..2892915c3 100644
--- a/helm/software/components/ng_kernel/nReference.ml
+++ b/helm/software/components/ng_kernel/nReference.ml
@@ -18,8 +18,8 @@ type spec =
  | Def of int (* height *)
  | Fix of int * int * int (* fixno, recparamno, height *)
  | CoFix of int
- | Ind of bool * int (* inductive, indtyno *)
- | Con of int * int (* indtyno, constrno *)
+ | Ind of bool * int * int (* inductive, indtyno, leftno *)
+ | Con of int * int * int  (* indtyno, constrno, leftno  *)
 
 type reference = Ref of NUri.uri * spec
 
@@ -64,12 +64,14 @@ let reference_of_string =
     let h = int_of_string s_h in
     i,j,h
   in
+(*
   let get2 s dot =
     let comma = String.rindex s ',' in
     let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
     let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
     i,j
   in
+*)
   let get1 s dot =
     let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
     i
@@ -88,8 +90,8 @@ fun s ->
         | "def" -> let i = get1 s dot in Ref (u, Def i)
         | "fix" -> let i,j,h = get3 s dot in Ref (u, Fix (i,j,h))
         | "cfx" -> let i = get1 s dot in Ref (u, CoFix (i))
-        | "ind" -> let b,i = get2 s dot in Ref (u, Ind (b=1,i))
-        | "con" -> let i,j = get2 s dot in Ref (u, Con (i,j))
+        | "ind" -> let b,i,l = get3 s dot in Ref (u, Ind (b=1,i,l))
+        | "con" -> let i,j,l = get3 s dot in Ref (u, Con (i,j,l))
         | _ -> raise Not_found
       with Not_found -> raise (IllFormedReference (lazy s))
     in
@@ -108,13 +110,15 @@ let string_of_reference (Ref (u,indinfo)) =
       s2 ^ ".fix(" ^ string_of_int i ^ "," ^ 
       string_of_int j ^ "," ^ string_of_int h ^ ")"
   | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
-  | Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")"
-  | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+  | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^
+      "," ^ string_of_int l ^ ")"
+  | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ 
+      "," ^ string_of_int l ^ ")"
 ;;
 
 let mk_constructor j = function
-  | Ref (u, Ind (_,i)) -> 
-      reference_of_string (string_of_reference (Ref (u, Con (i,j))))
+  | Ref (u, Ind (_,i,l)) -> 
+      reference_of_string (string_of_reference (Ref (u, Con (i,j,l))))
   | _ -> assert false
 ;;
 
diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli
index fcb12a995..703d32d02 100644
--- a/helm/software/components/ng_kernel/nReference.mli
+++ b/helm/software/components/ng_kernel/nReference.mli
@@ -15,11 +15,11 @@ exception IllFormedReference of string Lazy.t
 
 type spec = 
  | Decl 
- | Def of int (* height *)
- | Fix of int * int * int (* fixno, recparamno, height *)
+ | Def of int              (* height *)
+ | Fix of int * int * int  (* fixno, recparamno, height *)
  | CoFix of int
- | Ind of bool * int (* inductive, indtyno *)
- | Con of int * int (* indtyno, constrno *)
+ | Ind of bool * int * int (* inductive, indtyno, leftno *)
+ | Con of int * int * int  (* indtyno, constrno, leftno  *)
 
 type reference = private Ref of NUri.uri * spec
 
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 096834d40..aa546d773 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -646,29 +646,34 @@ let convert_term uri t =
                NCic.Const (reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
     | Cic.MutInd (curi, tyno, ens) -> 
-       let is_inductive =
+       let is_inductive, lno =
         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-           Cic.InductiveDefinition ([],_,_,_) -> true
-         | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+           Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+         | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
          | _ -> assert false
        in
         aux_ens k curi octx ctx n_fix uri ens
-         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
+       let lno =
+        match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+           Cic.InductiveDefinition (_,_,lno,_) -> lno
+         | _ -> assert false
+       in
        aux_ens k curi octx ctx n_fix uri ens
-        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
     | Cic.Var (curi, ens) ->
        (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
            Cic.Variable (_,Some bo,_,_,_) ->
             aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
          | _ -> assert false)
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
-        let is_inductive =
+        let is_inductive,lno =
          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-            Cic.InductiveDefinition ([],_,_,_) -> true
-          | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+            Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+          | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
           | _ -> assert false in
-        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
         let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         let branches, fixpoints =