Reordering Termops w.r.t. Evd and Namegen in engine folder.

5 files changed, 23 insertions, 13 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 9ce5af819..9cc6d9109 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,9 +1,9 @@
 Logic_monad
-Termops
 Namegen
 UState
 Evd
 Sigma
+Termops
 Proofview_monad
 Evarutil
 Proofview
diff --git a/engine/evd.ml b/engine/evd.ml
index bde0182cc..d8a658e3e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Termops
 open Environ
 open Globnames
 open Context.Named.Declaration
@@ -1264,7 +1263,9 @@ let protect f x =
   try f x
   with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
 
-let print_constr a = protect print_constr a
+let (f_print_constr, print_constr_hook) = Hook.make ()
+
+let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a
 
 let pr_meta_map mmap =
   let pr_name = function
@@ -1422,11 +1423,11 @@ let pr_evar_constraints pbs =
       Namegen.make_all_name_different env
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env t1 ++ spc () ++
+      Hook.get f_print_constr env t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ print_constr_env env t2
+      spc () ++ Hook.get f_print_constr env t2
   in
   prlist_with_sep fnl pr_evconstr pbs
 
diff --git a/engine/evd.mli b/engine/evd.mli
index b47b389d1..5c9effd4b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -607,6 +607,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
 (** {5 Debug pretty-printers} *)
 
+val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t
 val pr_evar_info : evar_info -> Pp.std_ppcmds
 val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 92a915111..e56ec2877 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -21,7 +21,6 @@ open Nameops
 open Libnames
 open Globnames
 open Environ
-open Termops
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -78,6 +77,10 @@ let is_constructor id =
   with Not_found ->
     false
 
+let is_section_variable id =
+  try let _ = Global.lookup_named id in true
+  with Not_found -> false
+
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
@@ -203,8 +206,8 @@ let visible_ids (nenv, c) =
     if p > n && not (Int.Set.mem p vseen) then
       let vseen = Int.Set.add p vseen in
       let name =
-        try Some (lookup_name_of_rel (p - n) nenv)
-        with Not_found ->
+        try Some (List.nth nenv (p - n - 1))
+        with Invalid_argument _ | Failure _ ->
           (* Unbound index: may happen in debug and actually also
              while computing temporary implicit arguments of an
              inductive type *)
@@ -290,14 +293,18 @@ let next_name_away_with_default_using_types default na avoid t =
 let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env =
-  let avoid = ref (ids_of_named_context (named_context env)) in
-  process_rel_context
+  (** FIXME: this is inefficient, but only used in printing *)
+  let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
+  let sign = named_context_val env in
+  let rels = rel_context env in
+  let env0 = reset_with_named_context sign env in
+  Context.Rel.fold_outside
     (fun decl newenv ->
        let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (RelDecl.set_name (Name id) decl) newenv)
-    env
+    rels ~init:env0
 
 (* 5- Looks for next fresh name outside a list; avoids also to use names that
    would clash with short name of global references; if name is already used,
@@ -377,12 +384,12 @@ let rename_bound_vars_as_displayed avoid env c =
 	let na',avoid' =
           compute_displayed_name_in
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
-	mkProd (na', c1, rename avoid' (add_name na' env) c2)
+	mkProd (na', c1, rename avoid' (na' :: env) c2)
     | LetIn (na,c1,t,c2) ->
 	let na',avoid' =
           compute_displayed_let_name_in
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
-	mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+	mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
     | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
     | _ -> c
   in
diff --git a/engine/termops.ml b/engine/termops.ml
index 5327f1829..298302815 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -101,6 +101,7 @@ let term_printer = ref (fun _ -> pr_constr)
 let print_constr_env t = !term_printer t
 let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
+let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c)
 
 let pr_var_decl env decl =
   let open NamedDecl in