Merge branch 'v8.5'

5 files changed, 55 insertions, 42 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0ab9f89ffa..ddbde9d385 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
 #   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
+#   define print_lint(i)  /*if (drawinstr)*/ printf("%ld\n",i)
 # else 
 #   define print_instr(s) 
 #   define print_int(i) 
+#   define print_lint(i)
 #endif
 
 /* GC interface */
@@ -795,12 +797,12 @@ value coq_interprete
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[index];
 	}
 	  Next;
@@ -957,7 +959,7 @@ value coq_interprete
 	    sp -= nargs;
 	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
 	    *--sp = accu;
-	    print_int(nargs);
+	    print_lint(nargs);
 	    coq_extra_args = nargs;
 	    pc = Code_val(coq_env);
 	    goto check_stacks;
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e823c01b17..e2b1d3fd9c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -475,7 +475,7 @@ let map_with_binders g f l c0 = match kind c0 with
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
   match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
@@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
    not taken into account *)
 
 let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
-  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+  compare_head_gen_leq_with kind kind  eq_universes leq_sorts eq leq t1 t2
 
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
+   compare the immediate subterms of [c1] of [c2] if needed, [u] to
+   compare universe instances and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account.
+
+   [compare_head_gen_with] is a variant taking kind-of-term functions,
+   to expose subterms of [c1] and [c2], as arguments. *)
+
+let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq eq t1 t2
 
 let compare_head_gen eq_universes eq_sorts eq t1 t2 =
   compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
@@ -536,14 +542,6 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
-let rec equal_with kind1 kind2 m n =
-  (* note that pointer equality is not sufficient to ensure equality
-     up to [eq_evars], because we may evaluates evars of [m] and [n]
-     in different evar contexts. *)
-  let req_constr m n = equal_with kind1 kind2 m n in
-  compare_head_gen_with kind1 kind2
-    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
-
 let eq_constr_univs univs m n =
   if m == n then true
   else 
@@ -567,7 +565,7 @@ let leq_constr_univs univs m n =
     let rec compare_leq m n =
       compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
-      compare_leq m n
+    compare_leq m n
 
 let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	     true)
+	if Univ.check_eq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -618,7 +616,7 @@ let leq_constr_univs_infer univs m n =
       compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let always_true _ _ = true
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 67d1adedf6..e6a3e71f89 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,14 +203,6 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
-(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
-    alpha, casts, application grouping, and using [k1] to expose the
-    head of [a] and [k2] to expose the head of [b]. *)
-val equal_with :
-  (constr -> (constr,types) kind_of_term) ->
-  (constr -> (constr,types) kind_of_term) ->
-  constr -> constr -> bool
-
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
@@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
+(** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
+    like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
+    is used,rather than {!kind}, to expose the immediate subterms of
+    [c1] (resp. [c2]). *)
+val compare_head_gen_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
diff --git a/kernel/names.ml b/kernel/names.ml
index 4ccf5b60ae..480b37e897 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -33,9 +33,9 @@ struct
 
   let hash = String.hash
 
-  let check_soft x =
+  let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
@@ -48,6 +48,11 @@ struct
     let s = String.copy s in
     String.hcons s
 
+  let of_string_soft s =
+    let () = check_soft ~warn:false s in
+    let s = String.copy s in
+    String.hcons s
+
   let to_string id = String.copy id
 
   let print id = str id
diff --git a/kernel/names.mli b/kernel/names.mli
index d82043da1a..92ee58f260 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -29,7 +29,11 @@ sig
 
   val of_string : string -> t
   (** Converts a string into an identifier. May raise [UserError _] if the
-      string is not valid. *)
+      string is not valid, or echo a warning if it contains invalid identifier
+      characters. *)
+
+  val of_string_soft : string -> t
+  (** Same as {!of_string} except that no warning is ever issued. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)