cicNotationUtil: in fresh_name_generator, "\eta" replaced with "eta", which is an...

[helm.git] / helm / software / components / acic_content / termAcicContent.ml

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 61e77c6fe12047b9efbe5939a362df8b088333fb..c350f38c41ab03c6a735643e676d2e53809e1009 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -109,7 +109,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type _ -> `Pi
+          | `Set | `Type _ | `NType _ -> `Pi
           | `Prop | `CProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
@@ -442,19 +442,22 @@ let set_active_interpretations ids =
 
 exception Interpretation_not_found
 
-let lookup_interpretations symbol =
+let lookup_interpretations ?(sorted=true) symbol =
   try
-   HExtlib.list_uniq
-    (List.sort Pervasives.compare
-     (List.map
-      (fun id ->
-        let (dsc, _, args, appl_pattern) =
-          try
-            Hashtbl.find !level2_patterns32 id
-          with Not_found -> assert false 
-        in
-        dsc, args, appl_pattern)
-      !(Hashtbl.find !interpretations symbol)))
+    let raw = 
+      List.map (
+        fun id ->
+          let (dsc, _, args, appl_pattern) =
+            try
+              Hashtbl.find !level2_patterns32 id
+            with Not_found -> assert false 
+          in
+          dsc, args, appl_pattern
+      )
+      !(Hashtbl.find !interpretations symbol)
+    in
+    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+              else raw
   with Not_found -> raise Interpretation_not_found
 
 let remove_interpretation id =