Fixing a normalizer inefficiency

src/basic/FStar.Ident.fst

@@ -88,3 +88,9 @@ instance hasrange_lident = {
   pos = (fun lid -> Class.HasRange.pos lid.ident);
   setPos = (fun rng id -> { id with ident = setPos rng id.ident });
 }
+instance deq_ident = {
+  (=?) = ident_equals;
+}
+instance deq_lident = {
+  (=?) = lid_equals;
+}

src/basic/FStar.Ident.fsti

@@ -18,6 +18,7 @@ module FStar.Ident
 open FStar.Compiler.Range
 open FStar.Class.Show
 open FStar.Class.HasRange
+open FStar.Class.Deq
 
 (** A (short) identifier for a local name.
  *  e.g. x in `fun x -> ...` *)
@@ -138,3 +139,5 @@ instance val showable_ident  : showable ident
 instance val showable_lident : showable lident
 instance val hasrange_ident  : hasRange ident
 instance val hasrange_lident : hasRange lident
+instance val deq_ident  : deq ident
+instance val deq_lident : deq lident

src/data/FStar.Compiler.Path.fst

@@ -32,4 +32,4 @@ let search_forest #a #q {| deq a |} p f =
     | [] -> def
     | (r, q)::rs -> if p `is_under` r then q else aux rs
   in
-  aux roots
+  aux roots

src/parser/FStar.Parser.Dep.fst

@@ -125,7 +125,7 @@ let module_name_of_file f =
     | Some longname ->
       longname
     | None ->
-      raise_err (Errors.Fatal_NotValidFStarFile, (Util.format1 "not a valid FStar file: %s" f))
+      raise_err (Errors.Fatal_NotValidFStarFile, (Util.format1 "Not a valid FStar file: '%s'" f))
 
 (* In public interface *)
 let lowercase_module_name f = String.lowercase (module_name_of_file f)

src/syntax/FStar.Syntax.Syntax.fst

@@ -146,6 +146,10 @@ instance deq_fv : deq lident =
   deq_instance_from_cmp (fun x y -> Order.order_from_int (order_fv x y))
 instance deq_univ_name : deq univ_name =
   deq_instance_from_cmp (fun x y -> Order.order_from_int (order_univ_name x y))
+instance deq_delta_depth : deq delta_depth = {
+  (=?) = (fun x y -> x = y);
+}
+
 instance ord_bv : ord bv =
   ord_instance_from_cmp (fun x y -> Order.order_from_int (order_bv x y))
 instance ord_ident : ord ident =
@@ -510,4 +514,4 @@ instance deq_lazy_kind : deq lazy_kind = {
           | Lazy_embedding _, _
           | _, Lazy_embedding _ -> false
           | _ -> false);
-}
+}