compile-time feature PROFV to profile validation without sort inclusion

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 5a726ca9703b732041fe5a0f0f09ef5536de5890..f597f6cf1db3fb8e306d8e1112543990b6e9074a 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -207,9 +207,6 @@ let xlate_entity err f st lst = function
                let y = attrs_for_decl yw in
                UH.add henv (uri_of_qid qid) (y, lenv);
               let t = add_proj yw lenv ww in
-(*
-           print_newline (); CrgOutput.pp_term print_string t;
-*)
                let na = E.node_attrs ~apix:lst.line () in
               let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
 IFDEF TRACE THEN
@@ -226,12 +223,13 @@ ELSE () END;
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
-            let f _ ww =
+            let f yw ww =
               let f yv vv =
                   UH.add henv (uri_of_qid qid) (yv, lenv);
                   let t = add_proj yv lenv (D.TCast (ww, vv)) in
 (*
-           print_newline (); CrgOutput.pp_term print_string t;
+                  let lenv0 = D.set_layer C.start N.one lenv in
+                  let t = D.TCast (add_proj yw lenv0 ww, add_proj yv lenv vv) in
 *)
                   let na = E.node_attrs ~apix:lst.line () in
                   let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in