Merge branch 'v8.5'

3 files changed, 7 insertions, 17 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 40409fe7fd..60239ebfe2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -945,7 +945,7 @@ let update_sigma_env evd env =
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
-let conversion_gen env evd pb t u =
+let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
     Reduction.trans_conv_universes 
@@ -955,14 +955,8 @@ let conversion_gen env evd pb t u =
      full_transparent_state ~evars:(existential_opt_value evd) env 
       (UState.ugraph evd.universes) t u
 
-(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
-(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
-
-let conversion env d pb t u =
-  conversion_gen env d pb t u; d
-
 let test_conversion env d pb t u =
-  try conversion_gen env d pb t u; true
+  try test_conversion_gen env d pb t u; true
   with _ -> false
 
 exception UniversesDiffer = UState.UniversesDiffer
diff --git a/engine/evd.mli b/engine/evd.mli
index 3a95b77f06..25d8a8c3d2 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -571,14 +571,11 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
   Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
-  Conversion w.r.t. an evar map: might generate universe unifications 
-  that are kept in the evarmap.
-  Raises [NotConvertible]. *)
-
-val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
+  Conversion w.r.t. an evar map, not unifying universes. See 
+  [Reductionops.infer_conv] for conversion up-to universes. *)
 
 val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** This one forgets about the assignemts of universes. *)
+(** WARNING: This does not allow unification of universes *)
 
 val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 (** Syntactic equality up to universes, recording the associated constraints *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 0901d81e9e..a00d9ccd14 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -32,9 +32,8 @@ type t =
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.universe_set; 
-   (** The subset of unification variables that
-        can be instantiated with algebraic universes as they appear in types 
-        and universe instances only. *)
+   (** The subset of unification variables that can be instantiated with
+        algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
  }