...

[helm.git] / matitaB / components / ng_cic_content / interpretations.ml

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 226eecdfde7800c7d06bbd2868acd7c215398902..75f46943052cc16868f64d102fd5255b279042b0 100644 (file)
--- 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 =