From dfb64dda51f7eea174e41129c8d2e0c3559298ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Apr 2015 08:35:57 +0200
Subject: Fixing bug #4190.

The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
---
 kernel/names.ml  | 9 +++++++--
 kernel/names.mli | 6 +++++-
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'kernel')

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. *)
-- 
cgit v1.2.3


From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 18:51:48 +0200
Subject: Tactical `progress` compares term up to potentially equalisable
 universes.

Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.

As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.---
 kernel/constr.ml  | 54 ++++++++++++++++++++++++++----------------------------
 kernel/constr.mli | 20 ++++++++++++--------
 2 files changed, 38 insertions(+), 36 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


From 62b0708ebfda01e377c4e6e229be4388a96cbecc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Apr 2015 11:21:35 +0200
Subject: Fix some ill-typed debugging code in the VM.

---
 kernel/byterun/coq_interp.c | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel')

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;
-- 
cgit v1.2.3