X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;fp=matitaB%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=75f46943052cc16868f64d102fd5255b279042b0;hb=4e89ae4ac9b001c0479d68d9f74fe81fca6ecd2d;hp=226eecdfde7800c7d06bbd2868acd7c215398902;hpb=76058a686dc58780de9ce8915ece239014bb2ff5;p=helm.git

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 226eecdfd..75f469430 100644
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -89,7 +89,7 @@ let level_of_uri u =
 let find_level2_patterns32 status pid =
  IntMap.find pid status#interp_db.level2_patterns32
 
-let instantiate32 env symbol args =
+let instantiate32 env symbol dsc args =
   let rec instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = 
@@ -112,7 +112,7 @@ let instantiate32 env symbol args =
         in
         add_lambda t (n - count_lambda t)
   in
-  let head = Ast.Symbol (symbol, None) in
+  let head = Ast.Symbol (symbol, Some (None, dsc)) in
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
@@ -338,12 +338,12 @@ let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term =
             term
         ) env
       in
-      let _, symbol, args, _ =
+      let dsc, symbol, args, _ =
         try
          find_level2_patterns32 status pid
         with Not_found -> assert false
       in
-      instantiate32 env symbol args 
+      instantiate32 env symbol dsc args 
 ;;
 
 let nmap_context0 status ~metasenv ~subst context =