From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 29 Oct 2009 19:50:22 +0000 (+0000)
Subject: - dual_rg: renamed to complete_rg [as suggested in the ToCL documentation]
X-Git-Tag: make_still_working~3224
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da715664068e859d20ab81fd6969e64d58c0f57e;p=helm.git

- dual_rg: renamed to complete_rg [as suggested in the ToCL documentation]
- Makefile: "lddl" entry generates lddl.tar.bz2
---

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 1cf0b734e..00b1db36f 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -114,23 +114,26 @@ basic_rg/brgUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \
 basic_rg/brgUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \
     basic_rg/brgType.cmx basic_rg/brgReduction.cmx \
     basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi 
-dual_rg/drg.cmo: common/entity.cmx 
-dual_rg/drg.cmx: common/entity.cmx 
-dual_rg/drgOutput.cmi: common/library.cmi dual_rg/drg.cmx 
-dual_rg/drgOutput.cmo: lib/nUri.cmi common/library.cmi common/hierarchy.cmi \
-    common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi 
-dual_rg/drgOutput.cmx: lib/nUri.cmx common/library.cmx common/hierarchy.cmx \
-    common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi 
-dual_rg/drgAut.cmi: common/entity.cmx dual_rg/drg.cmx automath/aut.cmx 
-dual_rg/drgAut.cmo: lib/nUri.cmi common/entity.cmx dual_rg/drg.cmx \
-    lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi 
-dual_rg/drgAut.cmx: lib/nUri.cmx common/entity.cmx dual_rg/drg.cmx \
-    lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi 
-dual_rg/drgBrg.cmi: dual_rg/drg.cmx basic_rg/brg.cmx 
-dual_rg/drgBrg.cmo: common/entity.cmx dual_rg/drg.cmx lib/cps.cmx \
-    basic_rg/brg.cmx dual_rg/drgBrg.cmi 
-dual_rg/drgBrg.cmx: common/entity.cmx dual_rg/drg.cmx lib/cps.cmx \
-    basic_rg/brg.cmx dual_rg/drgBrg.cmi 
+complete_rg/crg.cmo: common/entity.cmx 
+complete_rg/crg.cmx: common/entity.cmx 
+complete_rg/crgOutput.cmi: common/library.cmi complete_rg/crg.cmx 
+complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \
+    common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+    complete_rg/crgOutput.cmi 
+complete_rg/crgOutput.cmx: lib/nUri.cmx common/library.cmx \
+    common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+    complete_rg/crgOutput.cmi 
+complete_rg/crgAut.cmi: common/entity.cmx complete_rg/crg.cmx \
+    automath/aut.cmx 
+complete_rg/crgAut.cmo: lib/nUri.cmi common/entity.cmx complete_rg/crg.cmx \
+    lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi 
+complete_rg/crgAut.cmx: lib/nUri.cmx common/entity.cmx complete_rg/crg.cmx \
+    lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi 
+complete_rg/crgBrg.cmi: complete_rg/crg.cmx basic_rg/brg.cmx 
+complete_rg/crgBrg.cmo: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+    basic_rg/brg.cmx complete_rg/crgBrg.cmi 
+complete_rg/crgBrg.cmx: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+    basic_rg/brg.cmx complete_rg/crgBrg.cmi 
 toplevel/meta.cmo: common/entity.cmx 
 toplevel/meta.cmx: common/entity.cmx 
 toplevel/metaOutput.cmi: toplevel/meta.cmx 
@@ -160,8 +163,8 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \
     toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
     toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \
     common/library.cmi common/hierarchy.cmi common/entity.cmx \
-    dual_rg/drgOutput.cmi dual_rg/drgBrg.cmi dual_rg/drgAut.cmi \
-    dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \
+    complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi complete_rg/crgAut.cmi \
+    complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \
     basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \
     basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \
     basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \
@@ -170,8 +173,8 @@ toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
     toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
     toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \
     common/library.cmx common/hierarchy.cmx common/entity.cmx \
-    dual_rg/drgOutput.cmx dual_rg/drgBrg.cmx dual_rg/drgAut.cmx \
-    dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
+    complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx complete_rg/crgAut.cmx \
+    complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
     basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \
     basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \
     basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \
diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index d2edae23b..98a1c59c6 100644
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -50,7 +50,7 @@ xml-si-drg: $(MAIN).opt
 	$(H)$(XSLT) -o $(LDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml
 
 etc/make-html.sh xml/index.txt index:
-	@echo "  GENERATING INDEXES"
+	@echo "  GENERATE INDEXES"
 	$(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt
 	$(H)sed "s/^/make --no-print-directory /" xml/index.txt | sed s.ld:/.. > etc/make-html.sh
 
@@ -60,3 +60,7 @@ html: etc/make-html.sh
 
 test-html:
 	@$(MAKE) --no-print-directory $(XMLS:xml/%.xml=%)
+
+lddl: index
+	@echo "  GENERATE lddl.tar.bz2"
+	$(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml
diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common
index cd8713015..ca219ca66 100644
--- a/helm/software/lambda-delta/Makefile.common
+++ b/helm/software/lambda-delta/Makefile.common
@@ -2,6 +2,7 @@ H=@
 
 LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl
 LDDLDIR = /projects/helm/public_html/lambda-delta/static/lddl
+DOWNDIR = /projects/helm/public_html/lambda-delta/download
 
 DIRECTORIES = $(shell cat Make)
 
diff --git a/helm/software/lambda-delta/complete_rg/crg.ml b/helm/software/lambda-delta/complete_rg/crg.ml
new file mode 100644
index 000000000..6db1b5481
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crg.ml
@@ -0,0 +1,78 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+(* kernel version: complete, relative, global *)
+(* note          : fragment of complete lambda-delta serving as abstract layer *) 
+
+type uri = Entity.uri
+type id = Entity.id
+type attrs = Entity.attrs
+
+type bind = Abst of term list (* domains *)
+          | Abbr of term list (* bodies  *)
+          | Void of int       (* number of exclusions *)
+
+and term = TSort of attrs * int              (* attrs, hierarchy index *)
+         | TLRef of attrs * int * int        (* attrs, position indexes *)
+         | TGRef of attrs * uri              (* attrs, reference *)
+         | TCast of attrs * term * term      (* attrs, domain, element *)
+         | TAppl of attrs * term list * term (* attrs, arguments, function *)
+	 | TProj of attrs * lenv * term      (* attrs, closure, member *)
+	 | TBind of attrs * bind * term      (* attrs, binder, scope *)
+
+and lenv = ESort                        (* top *)
+         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
+         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
+
+type entity = term Entity.entity
+
+(* helpers ******************************************************************)
+
+let mk_uri root s =
+   String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"]
+
+let empty_lenv = ESort
+
+let push_bind f lenv a b = f (EBind (lenv, a, b))
+
+let push_proj f lenv a e = f (EProj (lenv, a, e))
+
+let push2 err f lenv attr ?t = match lenv, t with
+   | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
+   | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
+   | EBind (e, a, Void n), None    -> f (EBind (e, (attr :: a), Void (succ n)))
+   | _                             -> err ()
+
+(* this id not tail recursive *)
+let resolve_lref err f id lenv =
+   let rec aux f i k = function
+     | ESort            -> err ()
+     | EBind (tl, a, _) ->
+        let err kk = aux f (succ i) (k + kk) tl in
+	let f j = f i j (k + j) in
+	Entity.resolve err f id a
+     | EProj _          -> assert false (* TODO *)
+   in
+   aux f 0 0 lenv
+
+let rec get_name err f i j = function
+   | ESort                      -> err i
+   | EBind (tl, a, Abst [])     -> get_name err f i j tl
+   | EBind (tl, a, Abbr [])     -> get_name err f i j tl
+   | EBind (tl, a, Void 0)      -> get_name err f i j tl
+   | EBind (_, a, _) when i = 0 -> 
+      let err () = err i in
+      Entity.get_name err f j a
+   | EBind (tl, _, _)           -> 
+      get_name err f (pred i) j tl
+   | EProj (tl, _, e)           ->
+      let err i = get_name err f i j tl in 
+      get_name err f i j e
diff --git a/helm/software/lambda-delta/complete_rg/crgAut.ml b/helm/software/lambda-delta/complete_rg/crgAut.ml
new file mode 100644
index 000000000..267e2b403
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgAut.ml
@@ -0,0 +1,222 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module U = NUri
+module H = U.UriHash
+module C = Cps
+module Y = Entity
+module A = Aut
+module D = Crg
+
+(* qualified identifier: uri, name, qualifiers *)
+type qid = D.uri * D.id * D.id list
+
+type context = Y.attrs * D.term list
+
+type context_node = qid option (* context node: None = root *)
+
+type status = {
+   path: D.id list;          (* current section path *) 
+   node: context_node;       (* current context node *)
+   nodes: context_node list; (* context node list *)
+   line: int;                (* line number *)
+   mk_uri:Y.uri_generator    (* uri generator *) 
+}
+
+type resolver = Local of int
+              | Global of context
+
+let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
+
+let henv = H.create henv_size (* optimized global environment *)
+
+let hcnt = H.create hcnt_size (* optimized context *)
+
+(* Internal functions *******************************************************)
+
+let initial_status mk_uri =
+   H.clear henv; H.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri
+}
+
+let empty_cnt = [], []
+
+let add_abst (a, ws) id w = 
+   Y.Name (id, true) :: a, w :: ws 
+
+let lenv_of_cnt (a, ws) = 
+   D.push_bind C.start D.empty_lenv a (D.Abst ws)
+
+let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+
+let id_of_name (id, _, _) = id
+
+let mk_qid f st id path =
+   let str = String.concat "/" path in
+   let str = Filename.concat str id in 
+   let f str = f (U.uri_of_string str, id, path) in
+   f (st.mk_uri str)
+   
+let uri_of_qid (uri, _, _) = uri
+
+let complete_qid f st (id, is_local, qs) =
+   let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
+   let rec skip f = function
+      | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
+      | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
+      | _                                     -> f []
+   in
+   if is_local then f st.path else skip f (st.path, qs)
+
+let relax_qid f st (_, id, path) =
+   let f = function
+      | _ :: tl -> C.list_rev (mk_qid f st id) tl
+      | []      -> assert false
+   in
+   C.list_rev f path
+
+let relax_opt_qid f st = function
+   | None     -> f None
+   | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
+
+let resolve_gref err f st qid =
+   try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
+   with Not_found -> err qid 
+
+let resolve_gref_relaxed f st qid =
+(* this is not tail recursive *)   
+   let rec err qid = relax_qid (resolve_gref err f st) st qid in
+   resolve_gref err f st qid
+
+let get_cnt err f st = function
+   | None              -> f empty_cnt
+   | Some qid as node ->
+      try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
+      with Not_found -> err node
+
+let get_cnt_relaxed f st =
+(* this is not tail recursive *)   
+   let rec err node = relax_opt_qid (get_cnt err f st) st node in
+   get_cnt err f st st.node
+
+(* this is not tail recursive in the GRef branch *)
+let rec xlate_term f st lenv = function
+   | A.Sort s            -> 
+      let f h = f (D.TSort ([], h)) in
+      if s then f 0 else f 1
+   | A.Appl (v, t)       ->
+      let f vv tt = f (D.TAppl ([], [vv], tt)) in
+      let f vv = xlate_term (f vv) st lenv t in
+      xlate_term f st lenv v
+   | A.Abst (name, w, t) ->
+      let f ww = 
+         let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
+	 let f tt = f (D.TBind (a, b, tt)) in
+         let f lenv = xlate_term f st lenv t in
+	 D.push_bind f lenv a b
+      in
+      xlate_term f st lenv w
+   | A.GRef (name, args) ->
+      let map1 f = function
+	    | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
+	    | _              -> C.err ()
+      in
+      let map2 f = xlate_term f st lenv in
+      let g qid (a, _) =
+         let gref = D.TGRef ([], uri_of_qid qid) in
+	 match args, a with
+	    | [], [] -> f gref
+	    | _      -> 
+	       let f args = f (D.TAppl ([], args, gref)) in
+	       let f args = f (List.rev_map (map2 C.start) args) in
+	       let f a = C.list_rev_map_append f map1 a ~tail:args in
+	       C.list_sub_strict f a args
+      in
+      let g qid = resolve_gref_relaxed g st qid in
+      let err () = complete_qid g st name in
+      D.resolve_lref err (mk_lref f) (id_of_name name) lenv
+
+let xlate_entity err f st = function
+   | A.Section (Some (_, name))     ->
+      err {st with path = name :: st.path; nodes = st.node :: st.nodes}
+   | A.Section None            ->
+      begin match st.path, st.nodes with
+	 | _ :: ptl, nhd :: ntl -> 
+	    err {st with path = ptl; node = nhd; nodes = ntl}
+         | _                    -> assert false
+      end
+   | A.Context None            ->
+      err {st with node = None}
+   | A.Context (Some name)     ->
+      let f name = err {st with node = Some name} in
+      complete_qid f st name 
+   | A.Block (name, w)         ->
+      let f qid = 
+         let f cnt =
+	    let lenv = lenv_of_cnt cnt in
+	    let ww = xlate_term C.start st lenv w in
+	    H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
+	    err {st with node = Some qid}
+	 in
+         get_cnt_relaxed f st
+      in
+      complete_qid f st (name, true, [])
+   | A.Decl (name, w)          ->
+      let f cnt =
+         let a, ws = cnt in
+         let lenv = lenv_of_cnt cnt in
+	 let f qid = 
+            let ww = xlate_term C.start st lenv w in
+	    H.add henv (uri_of_qid qid) cnt;
+	    let t = match ws with
+	       | [] -> ww
+	       | _  -> D.TBind (a, D.Abst ws, ww)
+	    in
+(*
+	    print_newline (); CrgOutput.pp_term print_string t;
+*)
+	    let b = Y.Abst t in
+	    let entity = [Y.Mark st.line], uri_of_qid qid, b in
+	    f {st with line = succ st.line} entity
+	 in
+         complete_qid f st (name, true, [])
+      in
+      get_cnt_relaxed f st
+   | A.Def (name, w, trans, v) ->
+      let f cnt = 
+	 let a, ws = cnt in
+	 let lenv = lenv_of_cnt cnt in
+         let f qid = 
+            let ww = xlate_term C.start st lenv w in
+	    let vv = xlate_term C.start st lenv v in
+	    H.add henv (uri_of_qid qid) cnt;
+            let t = match ws with
+	       | [] -> D.TCast ([], ww, vv)
+	       | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
+	    in
+(*
+	    print_newline (); CrgOutput.pp_term print_string t;
+*)
+	    let b = Y.Abbr t in
+	    let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+	    let entity = a, uri_of_qid qid, b in
+	    f {st with line = succ st.line} entity
+	 in
+         complete_qid f st (name, true, [])
+      in
+      get_cnt_relaxed f st
+
+(* Interface functions ******************************************************)
+
+let initial_status mk_uri =
+   initial_status mk_uri
+
+let crg_of_aut = xlate_entity
diff --git a/helm/software/lambda-delta/complete_rg/crgAut.mli b/helm/software/lambda-delta/complete_rg/crgAut.mli
new file mode 100644
index 000000000..3f416a033
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgAut.mli
@@ -0,0 +1,17 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+type status
+
+val initial_status: Entity.uri_generator -> status 
+
+val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> 
+                status -> Aut.entity -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/crgBrg.ml b/helm/software/lambda-delta/complete_rg/crgBrg.ml
new file mode 100644
index 000000000..d07e6efbf
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgBrg.ml
@@ -0,0 +1,64 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module C = Cps
+module Y = Entity
+module D = Crg
+module B = Brg
+
+let rec lenv_fold_left map1 map2 x = function
+   | D.ESort            -> x
+   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
+   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
+
+let rec xlate_term f = function
+   | D.TSort (a, l)     -> f (B.Sort (a, l))
+   | D.TGRef (a, n)     -> f (B.GRef (a, n))
+   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
+   | D.TCast (a, u, t)  ->
+      let f uu tt = f (B.Cast (a, uu, tt)) in
+      let f uu = xlate_term (f uu) t in
+      xlate_term f u 
+   | D.TAppl (a, vs, t) ->
+      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
+      let f tt = C.list_fold_right f map vs tt in
+      xlate_term f t
+   | D.TProj (a, e, t)  ->
+      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
+      xlate_term f t
+   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
+      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
+   | D.TBind (a, b, t)  ->
+      let f tt = f (xlate_bind tt a b) in xlate_term f t
+
+and xlate_bind x a b =
+   let f a ns = a, ns in
+   let a, ns = Y.get_names f a in 
+   match b with
+      | D.Abst ws ->
+         let map x n w = 
+	    let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
+	 in
+	 List.fold_left2 map x ns ws 
+      | D.Abbr vs ->
+         let map x n v = 
+	    let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
+	 in
+	 List.fold_left2 map x ns vs
+      | D.Void _  ->
+         let map x n = B.Bind (B.Void (n :: a), x) in
+	 List.fold_left map x ns
+
+and xlate_proj x _ e =
+   lenv_fold_left xlate_bind xlate_proj x e
+
+let brg_of_crg f t =
+   f (xlate_term C.start t)
diff --git a/helm/software/lambda-delta/complete_rg/crgBrg.mli b/helm/software/lambda-delta/complete_rg/crgBrg.mli
new file mode 100644
index 000000000..db4e54221
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgBrg.mli
@@ -0,0 +1,12 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml
new file mode 100644
index 000000000..ecc4a33b1
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml
@@ -0,0 +1,148 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module P = Printf
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module X = Library
+module D = Crg
+
+(****************************************************************************)
+
+let pp_attrs out a =
+   let map = function
+      | Y.Name (s, true)  -> out (P.sprintf "%s;" s)
+      | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
+      | Y.Apix i          -> out (P.sprintf "+%i;" i)
+      | Y.Mark i          -> out (P.sprintf "@%i;" i)
+      | Y.Priv            -> out (P.sprintf "%s;" "~") 
+   in
+   List.iter map a
+
+let rec pp_term out = function
+   | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
+   | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
+   | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
+   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
+   | D.TProj (a, x, y) -> assert false
+   | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
+   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
+
+and pp_terms bg eg out vs =
+   let rec aux = function
+      | []      -> ()
+      | [v]     -> pp_term out v
+      | v :: vs -> pp_term out v; out ", "; aux vs
+   in
+   out bg; aux vs; out (eg ^ ".")
+
+and pp_bind out = function
+   | D.Abst x -> pp_terms "[:" "]" out x
+   | D.Abbr x -> pp_terms "[=" "]" out x
+   | D.Void x -> out (P.sprintf "[%u]" x)
+
+let rec pp_lenv out = function
+   | D.ESort           -> ()
+   | D.EProj (x, a, y) -> assert false
+   | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
+
+(****************************************************************************)
+
+let rec list_iter map l out tab = match l with
+   | []       -> ()
+   | hd :: tl -> map hd out tab; list_iter map tl out tab
+
+let list_rev_iter map e ns l out tab =
+   let rec aux err f e = function
+      | [], []            -> f e
+      | n :: ns, hd :: tl -> 
+        let f e =
+(*	
+           pp_lenv print_string e; print_string " |- "; 
+	   pp_term print_string hd; print_newline ();
+*)
+	   map e hd out tab; f (D.push2 C.err C.start e n ~t:hd)
+	in
+	aux err f e (ns, tl) 
+      | _                 -> err ()
+   in
+   ignore (aux C.err C.start e (ns, l))
+
+let lenv_iter map1 map2 l out tab = 
+   let rec aux f = function
+      | D.ESort              -> f ()
+      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
+      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
+   in 
+   aux C.start l
+
+let rec exp_term e t out tab = match t with
+   | D.TSort (a, l)       ->
+      let a =
+         let err _ = a in
+         let f s = Y.Name (s, true) :: a in
+	 H.get_sort err f l
+      in
+      let attrs = [X.position l; X.name a] in
+      X.tag X.sort attrs out tab
+   | D.TLRef (a, i, j)    ->
+      let a = 
+         let err _ = a in
+	 let f n r = Y.Name (n, r) :: a in
+         D.get_name err f i j e
+      in
+      let attrs = [X.position i; X.offset j; X.name a] in
+      X.tag X.lref attrs out tab
+   | D.TGRef (a, n)       ->
+      let a = Y.Name (U.name_of_uri n, true) :: a in
+      let attrs = [X.uri n; X.name a] in
+      X.tag X.gref attrs out tab
+   | D.TCast (a, u, t)    ->
+      let attrs = [] in
+      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+      exp_term e t out tab
+   | D.TAppl (a, vs, t)   ->
+      let attrs = [X.arity (List.length vs)] in
+      X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+      exp_term e t out tab
+   | D.TProj (a, lenv, t) ->
+      let attrs = [] in
+      X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+      exp_term (D.push_proj C.start e a lenv) t out tab
+   | D.TBind (a, b, t) ->
+      exp_bind e a b out tab; 
+      exp_term (D.push_bind C.start e a b) t out tab 
+
+and exp_bind e a b out tab = 
+   let f a ns = a, ns in
+   let a, ns = Y.get_names f a in 
+   match b with
+      | D.Abst ws ->
+         let e = D.push_bind C.start e a (D.Abst []) in
+	 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+         X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+      | D.Abbr vs ->
+         let e = D.push_bind C.start e a (D.Abbr []) in
+         let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+      | D.Void n ->
+         let attrs = [X.name a; X.mark a; X.arity n] in
+         X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+   let attrs = [] in
+   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(****************************************************************************)
+
+let export_term = exp_term D.empty_lenv
diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.mli b/helm/software/lambda-delta/complete_rg/crgOutput.mli
new file mode 100644
index 000000000..4d3f747fd
--- /dev/null
+++ b/helm/software/lambda-delta/complete_rg/crgOutput.mli
@@ -0,0 +1,14 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+val export_term: Crg.term -> Library.pp
+
+val pp_term: (string -> unit) -> Crg.term -> unit
diff --git a/helm/software/lambda-delta/complete_rg/drg.ml b/helm/software/lambda-delta/complete_rg/drg.ml
deleted file mode 100644
index 87e973ca8..000000000
--- a/helm/software/lambda-delta/complete_rg/drg.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-(* kernel version: dual, relative, global *)
-(* note          : fragment of dual lambda-delta serving as abstract layer *) 
-
-type uri = Entity.uri
-type id = Entity.id
-type attrs = Entity.attrs
-
-type bind = Abst of term list (* domains *)
-          | Abbr of term list (* bodies  *)
-          | Void of int       (* number of exclusions *)
-
-and term = TSort of attrs * int              (* attrs, hierarchy index *)
-         | TLRef of attrs * int * int        (* attrs, position indexes *)
-         | TGRef of attrs * uri              (* attrs, reference *)
-         | TCast of attrs * term * term      (* attrs, domain, element *)
-         | TAppl of attrs * term list * term (* attrs, arguments, function *)
-	 | TProj of attrs * lenv * term      (* attrs, closure, member *)
-	 | TBind of attrs * bind * term      (* attrs, binder, scope *)
-
-and lenv = ESort                        (* top *)
-         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
-         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
-
-type entity = term Entity.entity
-
-(* helpers ******************************************************************)
-
-let mk_uri root s =
-   String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"]
-
-let empty_lenv = ESort
-
-let push_bind f lenv a b = f (EBind (lenv, a, b))
-
-let push_proj f lenv a e = f (EProj (lenv, a, e))
-
-let push2 err f lenv attr ?t = match lenv, t with
-   | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
-   | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
-   | EBind (e, a, Void n), None    -> f (EBind (e, (attr :: a), Void (succ n)))
-   | _                             -> err ()
-
-(* this id not tail recursive *)
-let resolve_lref err f id lenv =
-   let rec aux f i k = function
-     | ESort            -> err ()
-     | EBind (tl, a, _) ->
-        let err kk = aux f (succ i) (k + kk) tl in
-	let f j = f i j (k + j) in
-	Entity.resolve err f id a
-     | EProj _          -> assert false (* TODO *)
-   in
-   aux f 0 0 lenv
-
-let rec get_name err f i j = function
-   | ESort                      -> err i
-   | EBind (tl, a, Abst [])     -> get_name err f i j tl
-   | EBind (tl, a, Abbr [])     -> get_name err f i j tl
-   | EBind (tl, a, Void 0)      -> get_name err f i j tl
-   | EBind (_, a, _) when i = 0 -> 
-      let err () = err i in
-      Entity.get_name err f j a
-   | EBind (tl, _, _)           -> 
-      get_name err f (pred i) j tl
-   | EProj (tl, _, e)           ->
-      let err i = get_name err f i j tl in 
-      get_name err f i j e
diff --git a/helm/software/lambda-delta/complete_rg/drgAut.ml b/helm/software/lambda-delta/complete_rg/drgAut.ml
deleted file mode 100644
index 4b17faaa1..000000000
--- a/helm/software/lambda-delta/complete_rg/drgAut.ml
+++ /dev/null
@@ -1,222 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module U = NUri
-module H = U.UriHash
-module C = Cps
-module Y = Entity
-module A = Aut
-module D = Drg
-
-(* qualified identifier: uri, name, qualifiers *)
-type qid = D.uri * D.id * D.id list
-
-type context = Y.attrs * D.term list
-
-type context_node = qid option (* context node: None = root *)
-
-type status = {
-   path: D.id list;          (* current section path *) 
-   node: context_node;       (* current context node *)
-   nodes: context_node list; (* context node list *)
-   line: int;                (* line number *)
-   mk_uri:Y.uri_generator    (* uri generator *) 
-}
-
-type resolver = Local of int
-              | Global of context
-
-let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-
-let henv = H.create henv_size (* optimized global environment *)
-
-let hcnt = H.create hcnt_size (* optimized context *)
-
-(* Internal functions *******************************************************)
-
-let initial_status mk_uri =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri
-}
-
-let empty_cnt = [], []
-
-let add_abst (a, ws) id w = 
-   Y.Name (id, true) :: a, w :: ws 
-
-let lenv_of_cnt (a, ws) = 
-   D.push_bind C.start D.empty_lenv a (D.Abst ws)
-
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
-
-let id_of_name (id, _, _) = id
-
-let mk_qid f st id path =
-   let str = String.concat "/" path in
-   let str = Filename.concat str id in 
-   let f str = f (U.uri_of_string str, id, path) in
-   f (st.mk_uri str)
-   
-let uri_of_qid (uri, _, _) = uri
-
-let complete_qid f st (id, is_local, qs) =
-   let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
-   let rec skip f = function
-      | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
-      | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
-      | _                                     -> f []
-   in
-   if is_local then f st.path else skip f (st.path, qs)
-
-let relax_qid f st (_, id, path) =
-   let f = function
-      | _ :: tl -> C.list_rev (mk_qid f st id) tl
-      | []      -> assert false
-   in
-   C.list_rev f path
-
-let relax_opt_qid f st = function
-   | None     -> f None
-   | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
-
-let resolve_gref err f st qid =
-   try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
-   with Not_found -> err qid 
-
-let resolve_gref_relaxed f st qid =
-(* this is not tail recursive *)   
-   let rec err qid = relax_qid (resolve_gref err f st) st qid in
-   resolve_gref err f st qid
-
-let get_cnt err f st = function
-   | None              -> f empty_cnt
-   | Some qid as node ->
-      try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
-      with Not_found -> err node
-
-let get_cnt_relaxed f st =
-(* this is not tail recursive *)   
-   let rec err node = relax_opt_qid (get_cnt err f st) st node in
-   get_cnt err f st st.node
-
-(* this is not tail recursive in the GRef branch *)
-let rec xlate_term f st lenv = function
-   | A.Sort s            -> 
-      let f h = f (D.TSort ([], h)) in
-      if s then f 0 else f 1
-   | A.Appl (v, t)       ->
-      let f vv tt = f (D.TAppl ([], [vv], tt)) in
-      let f vv = xlate_term (f vv) st lenv t in
-      xlate_term f st lenv v
-   | A.Abst (name, w, t) ->
-      let f ww = 
-         let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
-	 let f tt = f (D.TBind (a, b, tt)) in
-         let f lenv = xlate_term f st lenv t in
-	 D.push_bind f lenv a b
-      in
-      xlate_term f st lenv w
-   | A.GRef (name, args) ->
-      let map1 f = function
-	    | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
-	    | _              -> C.err ()
-      in
-      let map2 f = xlate_term f st lenv in
-      let g qid (a, _) =
-         let gref = D.TGRef ([], uri_of_qid qid) in
-	 match args, a with
-	    | [], [] -> f gref
-	    | _      -> 
-	       let f args = f (D.TAppl ([], args, gref)) in
-	       let f args = f (List.rev_map (map2 C.start) args) in
-	       let f a = C.list_rev_map_append f map1 a ~tail:args in
-	       C.list_sub_strict f a args
-      in
-      let g qid = resolve_gref_relaxed g st qid in
-      let err () = complete_qid g st name in
-      D.resolve_lref err (mk_lref f) (id_of_name name) lenv
-
-let xlate_entity err f st = function
-   | A.Section (Some (_, name))     ->
-      err {st with path = name :: st.path; nodes = st.node :: st.nodes}
-   | A.Section None            ->
-      begin match st.path, st.nodes with
-	 | _ :: ptl, nhd :: ntl -> 
-	    err {st with path = ptl; node = nhd; nodes = ntl}
-         | _                    -> assert false
-      end
-   | A.Context None            ->
-      err {st with node = None}
-   | A.Context (Some name)     ->
-      let f name = err {st with node = Some name} in
-      complete_qid f st name 
-   | A.Block (name, w)         ->
-      let f qid = 
-         let f cnt =
-	    let lenv = lenv_of_cnt cnt in
-	    let ww = xlate_term C.start st lenv w in
-	    H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
-	    err {st with node = Some qid}
-	 in
-         get_cnt_relaxed f st
-      in
-      complete_qid f st (name, true, [])
-   | A.Decl (name, w)          ->
-      let f cnt =
-         let a, ws = cnt in
-         let lenv = lenv_of_cnt cnt in
-	 let f qid = 
-            let ww = xlate_term C.start st lenv w in
-	    H.add henv (uri_of_qid qid) cnt;
-	    let t = match ws with
-	       | [] -> ww
-	       | _  -> D.TBind (a, D.Abst ws, ww)
-	    in
-(*
-	    DrgOutput.pp_term print_string t; print_newline ();
-*)
-	    let b = Y.Abst t in
-	    let entity = [Y.Mark st.line], uri_of_qid qid, b in
-	    f {st with line = succ st.line} entity
-	 in
-         complete_qid f st (name, true, [])
-      in
-      get_cnt_relaxed f st
-   | A.Def (name, w, trans, v) ->
-      let f cnt = 
-	 let a, ws = cnt in
-	 let lenv = lenv_of_cnt cnt in
-         let f qid = 
-            let ww = xlate_term C.start st lenv w in
-	    let vv = xlate_term C.start st lenv v in
-	    H.add henv (uri_of_qid qid) cnt;
-            let t = match ws with
-	       | [] -> D.TCast ([], ww, vv)
-	       | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
-	    in
-(*
-            Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid));
-*)
-	    let b = Y.Abbr t in
-	    let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
-	    let entity = a, uri_of_qid qid, b in
-	    f {st with line = succ st.line} entity
-	 in
-         complete_qid f st (name, true, [])
-      in
-      get_cnt_relaxed f st
-
-(* Interface functions ******************************************************)
-
-let initial_status mk_uri =
-   initial_status mk_uri
-
-let drg_of_aut = xlate_entity
diff --git a/helm/software/lambda-delta/complete_rg/drgAut.mli b/helm/software/lambda-delta/complete_rg/drgAut.mli
deleted file mode 100644
index 5de7f7e85..000000000
--- a/helm/software/lambda-delta/complete_rg/drgAut.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-type status
-
-val initial_status: Entity.uri_generator -> status 
-
-val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) -> 
-                status -> Aut.entity -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.ml b/helm/software/lambda-delta/complete_rg/drgBrg.ml
deleted file mode 100644
index 9ff63fb7c..000000000
--- a/helm/software/lambda-delta/complete_rg/drgBrg.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module C = Cps
-module Y = Entity
-module D = Drg
-module B = Brg
-
-let rec lenv_fold_left map1 map2 x = function
-   | D.ESort            -> x
-   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
-   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
-let rec xlate_term f = function
-   | D.TSort (a, l)     -> f (B.Sort (a, l))
-   | D.TGRef (a, n)     -> f (B.GRef (a, n))
-   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
-   | D.TCast (a, u, t)  ->
-      let f uu tt = f (B.Cast (a, uu, tt)) in
-      let f uu = xlate_term (f uu) t in
-      xlate_term f u 
-   | D.TAppl (a, vs, t) ->
-      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
-      let f tt = C.list_fold_right f map vs tt in
-      xlate_term f t
-   | D.TProj (a, e, t)  ->
-      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
-      xlate_term f t
-   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
-   | D.TBind (a, b, t)  ->
-      let f tt = f (xlate_bind tt a b) in xlate_term f t
-
-and xlate_bind x a b =
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst ws ->
-         let map x n w = 
-	    let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
-	 in
-	 List.fold_left2 map x ns ws 
-      | D.Abbr vs ->
-         let map x n v = 
-	    let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
-	 in
-	 List.fold_left2 map x ns vs
-      | D.Void _  ->
-         let map x n = B.Bind (B.Void (n :: a), x) in
-	 List.fold_left map x ns
-
-and xlate_proj x _ e =
-   lenv_fold_left xlate_bind xlate_proj x e
-
-let brg_of_drg f t =
-(*   
-   print_newline (); DrgOutput.pp_term print_string t;
-*)
-   f (xlate_term C.start t)
diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.mli b/helm/software/lambda-delta/complete_rg/drgBrg.mli
deleted file mode 100644
index 900dad95a..000000000
--- a/helm/software/lambda-delta/complete_rg/drgBrg.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-val brg_of_drg: (Brg.term -> 'a) -> Drg.term -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.ml b/helm/software/lambda-delta/complete_rg/drgOutput.ml
deleted file mode 100644
index 5cb9538dd..000000000
--- a/helm/software/lambda-delta/complete_rg/drgOutput.ml
+++ /dev/null
@@ -1,148 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module P = Printf
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module X = Library
-module D = Drg
-
-(****************************************************************************)
-
-let pp_attrs out a =
-   let map = function
-      | Y.Name (s, true)  -> out (P.sprintf "%s;" s)
-      | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
-      | Y.Apix i          -> out (P.sprintf "+%i;" i)
-      | Y.Mark i          -> out (P.sprintf "@%i;" i)
-      | Y.Priv            -> out (P.sprintf "%s;" "~") 
-   in
-   List.iter map a
-
-let rec pp_term out = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
-   | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
-   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
-   | D.TProj (a, x, y) -> assert false
-   | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
-
-and pp_terms bg eg out vs =
-   let rec aux = function
-      | []      -> ()
-      | [v]     -> pp_term out v
-      | v :: vs -> pp_term out v; out ", "; aux vs
-   in
-   out bg; aux vs; out (eg ^ ".")
-
-and pp_bind out = function
-   | D.Abst x -> pp_terms "[:" "]" out x
-   | D.Abbr x -> pp_terms "[=" "]" out x
-   | D.Void x -> out (P.sprintf "[%u]" x)
-
-let rec pp_lenv out = function
-   | D.ESort           -> ()
-   | D.EProj (x, a, y) -> assert false
-   | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
-
-(****************************************************************************)
-
-let rec list_iter map l out tab = match l with
-   | []       -> ()
-   | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
-   let rec aux err f e = function
-      | [], []            -> f e
-      | n :: ns, hd :: tl -> 
-        let f e =
-(*	
-           pp_lenv print_string e; print_string " |- "; 
-	   pp_term print_string hd; print_newline ();
-*)
-	   map e hd out tab; f (D.push2 C.err C.start e n ~t:hd)
-	in
-	aux err f e (ns, tl) 
-      | _                 -> err ()
-   in
-   ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab = 
-   let rec aux f = function
-      | D.ESort              -> f ()
-      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
-      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
-   in 
-   aux C.start l
-
-let rec exp_term e t out tab = match t with
-   | D.TSort (a, l)       ->
-      let a =
-         let err _ = a in
-         let f s = Y.Name (s, true) :: a in
-	 H.get_sort err f l
-      in
-      let attrs = [X.position l; X.name a] in
-      X.tag X.sort attrs out tab
-   | D.TLRef (a, i, j)    ->
-      let a = 
-         let err _ = a in
-	 let f n r = Y.Name (n, r) :: a in
-         D.get_name err f i j e
-      in
-      let attrs = [X.position i; X.offset j; X.name a] in
-      X.tag X.lref attrs out tab
-   | D.TGRef (a, n)       ->
-      let a = Y.Name (U.name_of_uri n, true) :: a in
-      let attrs = [X.uri n; X.name a] in
-      X.tag X.gref attrs out tab
-   | D.TCast (a, u, t)    ->
-      let attrs = [] in
-      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
-      exp_term e t out tab
-   | D.TAppl (a, vs, t)   ->
-      let attrs = [X.arity (List.length vs)] in
-      X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
-      exp_term e t out tab
-   | D.TProj (a, lenv, t) ->
-      let attrs = [] in
-      X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
-      exp_term (D.push_proj C.start e a lenv) t out tab
-   | D.TBind (a, b, t) ->
-      exp_bind e a b out tab; 
-      exp_term (D.push_bind C.start e a b) t out tab 
-
-and exp_bind e a b out tab = 
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst ws ->
-         let e = D.push_bind C.start e a (D.Abst []) in
-	 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
-         X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
-      | D.Abbr vs ->
-         let e = D.push_bind C.start e a (D.Abbr []) in
-         let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
-         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
-      | D.Void n ->
-         let attrs = [X.name a; X.mark a; X.arity n] in
-         X.tag X.void attrs out tab
-
-and exp_eproj e a lenv out tab =
-   let attrs = [] in
-   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
-
-(****************************************************************************)
-
-let export_term = exp_term D.empty_lenv
diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.mli b/helm/software/lambda-delta/complete_rg/drgOutput.mli
deleted file mode 100644
index e02161b13..000000000
--- a/helm/software/lambda-delta/complete_rg/drgOutput.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-val export_term: Drg.term -> Library.pp
-
-val pp_term: (string -> unit) -> Drg.term -> unit
diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 6f7d60e9c..12e639c56 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -20,12 +20,12 @@ module Y    = Entity
 module X    = Library
 module AP   = AutProcess
 module AO   = AutOutput
-module DA   = DrgAut
+module DA   = CrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
-module DO   = DrgOutput
-module DBrg = DrgBrg
+module DO   = CrgOutput
+module DBrg = CrgBrg
 module MBrg = MetaBrg
 module BrgO = BrgOutput
 module BrgR = BrgReduction
@@ -76,7 +76,7 @@ type kernel = Brg | Bag
 
 type kernel_entity = BrgEntity  of Brg.entity
                    | BagEntity  of Bag.entity
-		   | DrgEntity  of Drg.entity
+		   | CrgEntity  of Crg.entity
 		   | MetaEntity of Meta.entity
 
 let kernel = ref Brg
@@ -86,8 +86,8 @@ let print_counters st = match !kernel with
    | Bag -> BagO.print_counters C.start st.bagc
 
 let xlate f st entity = match !kernel, entity with
-   | Brg, DrgEntity e  -> 
-      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_drg e
+   | Brg, CrgEntity e  -> 
+      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
    | Brg, MetaEntity e -> 
       let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
    | Bag, MetaEntity e -> 
@@ -102,7 +102,7 @@ let pp_progress e =
       Y.mark err f a
    in
    match e with
-      | DrgEntity e -> Y.common f e
+      | CrgEntity e -> Y.common f e
       | BrgEntity e -> Y.common f e
       | BagEntity e -> Y.common f e      
       | MetaEntity e -> Y.common f e
@@ -114,7 +114,7 @@ let count_entity st = function
    | _            -> st
 
 let export_entity si g moch = function
-   | DrgEntity e  -> X.export_entity DO.export_term si g e
+   | CrgEntity e  -> X.export_entity DO.export_term si g e
    | BrgEntity e  -> X.export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with
@@ -125,12 +125,12 @@ let export_entity si g moch = function
 
 let type_check f st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
-   let ok _ (a, u, _) = f st a u in
+   let ok _ _ = f st in
    match k with
-      | BrgEntity entity     -> BrgU.type_check brg_err ok ~si g entity
-      | BagEntity entity     -> BagU.type_check ok ~si g entity
-      | DrgEntity (a, u, _)
-      | MetaEntity (a, u, _) -> f st a u
+      | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
+      | BagEntity entity -> BagU.type_check ok ~si g entity
+      | CrgEntity _
+      | MetaEntity _     -> f st
 
 (****************************************************************************)
 
@@ -146,7 +146,7 @@ let export = ref false
 let graph = ref (H.graph_of_string C.err C.start "Z2")
 let old = ref false
 
-let process_3 f st a u =
+let process_3 f st =
    f st
 
 let process_2 f st entity =
@@ -166,9 +166,9 @@ let process_0 f st entity =
       let frr mst = f {st with mst = mst} in
       let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in
       let err dst = f {st with dst = dst} in
-      let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in
+      let g dst e = process_1 f {st with dst = dst} (CrgEntity e) in
       if !old then MA.meta_of_aut frr h st.mst entity else 
-      DA.drg_of_aut err g st.dst entity
+      DA.crg_of_aut err g st.dst entity
    in
    let st = {st with ac = count AO.count_entity st.ac entity} in 
    if !preprocess then process_entity f st entity else f st entity
@@ -219,7 +219,7 @@ try
       if !L.level > 0 then T.utime_stamp "parsed";
       O.clear_reductions ();
       let mk_uri =
-         if !stage < 2 then Drg.mk_uri else
+         if !stage < 2 then Crg.mk_uri else
 	 match !kernel with
 	    | Brg -> Brg.mk_uri
 	    | Bag -> Bag.mk_uri
@@ -255,7 +255,7 @@ try
    let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in
    let help_m = " output intermediate representation (HAL)" in
-   let help_o = " use old abstract language instead of drg" in   
+   let help_o = " use old abstract language instead of crg" in   
    let help_p = " preprocess Automath source" in
    let help_r = " disable initial segment of URI hierarchy" in
    let help_s = "<number>  set translation stage (see above)" in