From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 3f924cfa14..196962354c 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -12,8 +12,8 @@
 open Pp
 open Names
 open Term
-open EConstr
 open Environ
+open EConstr
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
@@ -283,4 +283,4 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
-- 
cgit v1.2.3