From cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 27 Jul 2015 10:50:04 +0200
Subject: Fixing bug #3736 (anomaly instead of error/warning/silence on
 decidability scheme).

Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:

Set Decidable Equality Schemes.
Inductive a := A with b := B.

which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
---
 test-suite/bugs/closed/3736.v | 8 ++++++++
 toplevel/auto_ind_decl.ml     | 3 ++-
 toplevel/auto_ind_decl.mli    | 1 +
 toplevel/indschemes.ml        | 3 +++
 4 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3736.v

diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v
new file mode 100644
index 000000000..637b77cc5
--- /dev/null
+++ b/test-suite/bugs/closed/3736.v
@@ -0,0 +1,8 @@
+(* Check non-error failure in case of unsupported decidability scheme *)
+Local Set Decidable Equality Schemes.
+
+Inductive a := A with b := B.
+
+(* But fails with error if explicitly asked for the scheme *)
+
+Fail Scheme Equality for a.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f90508090..d1452fca2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -55,6 +55,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 let dl = Loc.ghost
 
@@ -921,7 +922,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 let make_eq_decidability mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    anomaly (Pp.str "Decidability lemma for mutual inductive types not supported");
+    raise DecidabilityMutualNotSupported;
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 807872988..20a3d5d74 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -23,6 +23,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fbc45b4ae..f8f062dad 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -180,6 +180,9 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
+    | DecidabilityMutualNotSupported ->
+        alarm what internal
+          (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
 	alarm what internal
 	  (str "Unknown exception during scheme creation: "++
-- 
cgit v1.2.3


From 9b690c608c2a48b26a8ac94325fe0008d438fb3b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 27 Jul 2015 11:03:11 +0200
Subject: Improving over 26aa224293 in reporting unexpected error during scheme
 creation.

This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
---
 toplevel/indschemes.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index f8f062dad..286d164c4 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -184,9 +184,8 @@ let try_declare_scheme what f internal names kn =
         alarm what internal
           (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
-	alarm what internal
-	  (str "Unknown exception during scheme creation: "++
-           str (Printexc.to_string e))
+        alarm what internal
+	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
-- 
cgit v1.2.3


From e46b3b6ab289f73abc240a765e81c2fe6220dce7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 27 Jul 2015 11:39:34 +0200
Subject: Slightly improving line break formatting in Info command.

---
 proofs/proofview.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6e653806b..de6d60567 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -648,7 +648,7 @@ let goodmod p m =
 
 let cycle n =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let n' = goodmod n l in
@@ -658,7 +658,7 @@ let cycle n =
 
 let swap i j =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -1057,7 +1057,7 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.set { solution = sigma; comb; }
   end
 
-- 
cgit v1.2.3


From c2a67e6f1cdd803b46a3ff4dc259c1cc57ade33f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 27 Jul 2015 14:02:50 +0200
Subject: Fixing #4305 (compatibility wrt 8.4 in not interpreting an
 abbreviation not bound to an applied constructor as itself but rather as a
 binding variable as it was the case for non-applied constructor). This was
 broken by e5c02503 while fixed #3483 (Not_found uncaught with a notation to a
 non-constructor).

---
 interp/constrintern.ml        |  2 +-
 test-suite/bugs/closed/4305.v | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4305.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 982d9bfe3..8c56d0ccf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for =
 	      let (argscs,_) = find_remaining_scopes pats [] g in
 	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
 	| NApp (NRef g,args) ->
-	      ensure_kind top loc g;
+	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
 	      let pats1,pats2 = List.chop nvars pats in
diff --git a/test-suite/bugs/closed/4305.v b/test-suite/bugs/closed/4305.v
new file mode 100644
index 000000000..39fc02d22
--- /dev/null
+++ b/test-suite/bugs/closed/4305.v
@@ -0,0 +1,17 @@
+(* Check fallback when an abbreviation is not interpretable as a pattern *)
+
+Notation foo := Type.
+
+Definition t :=
+  match 0 with
+  | S foo => foo
+  | _ => 0
+  end.
+
+Notation bar := (option Type).
+
+Definition u :=
+  match 0 with
+  | S bar => bar
+  | _ => 0
+  end.
-- 
cgit v1.2.3


From 6d8d39fd0a1c7dac1b6415660fd97fe3ad010ff7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 27 Jul 2015 18:19:56 +0200
Subject: Test for bug #2243.

---
 test-suite/bugs/closed/2243.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/2243.v

diff --git a/test-suite/bugs/closed/2243.v b/test-suite/bugs/closed/2243.v
new file mode 100644
index 000000000..6d45c9a09
--- /dev/null
+++ b/test-suite/bugs/closed/2243.v
@@ -0,0 +1,9 @@
+Inductive is_nul: nat -> Prop := X: is_nul 0.
+Section O.
+Variable u: nat.
+Variable H: is_nul u.
+Goal True.
+Proof.
+destruct H.
+Undo.
+revert H; intro H; destruct H.
-- 
cgit v1.2.3


From 71b101172275a7c5872f6e8e70f9c0185f93f828 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 28 Jul 2015 12:30:14 +0200
Subject: Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)

File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.

There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
---
 ide/ideutils.ml           |  2 +-
 lib/util.ml               | 11 +++++++++++
 lib/util.mli              |  3 +++
 toplevel/vernac.ml        | 13 -------------
 toplevel/vernacentries.ml | 10 ----------
 5 files changed, 15 insertions(+), 24 deletions(-)

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 67e4bdb0c..5892fb3d9 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -311,7 +311,7 @@ let read_buffer = Buffer.create maxread
     I/O Exceptions are propagated. *)
 
 let read_file name buf =
-  let ic = open_in name in
+  let ic = Util.open_utf8_file_in name in
   let len = ref 0 in
   try
     while len := input ic read_string 0 maxread; !len > 0 do
diff --git a/lib/util.ml b/lib/util.ml
index a8c25f745..a20dba0fc 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -132,3 +132,14 @@ let map_union f g = function
 type iexn = Exninfo.iexn
 
 let iraise = Exninfo.iraise
+
+let open_utf8_file_in fname =
+  let is_bom s =
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
+  in
+  let in_chan = open_in fname in
+  let s = "   " in
+  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
+  in_chan
diff --git a/lib/util.mli b/lib/util.mli
index 4fce809c2..1dc405fcb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
+
+val open_utf8_file_in : string -> in_channel
+(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 966b95201..266d8f9b4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -92,19 +92,6 @@ let disable_drop = function
 
 let user_error loc s = Errors.user_err_loc (loc,"_",str s)
 
-(* Open an utf-8 encoded file and skip the byte-order mark if any *)
-
-let open_utf8_file_in fname =
-  let is_bom s =
-    Int.equal (Char.code s.[0]) 0xEF &&
-    Int.equal (Char.code s.[1]) 0xBB &&
-    Int.equal (Char.code s.[2]) 0xBF
-  in
-  let in_chan = open_in fname in
-  let s = "   " in
-  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-  in_chan
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6c5f10c20..cfbdaccec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1841,16 +1841,6 @@ let vernac_load interp fname =
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
-  let open_utf8_file_in fname =
-    let is_bom s =
-      Int.equal (Char.code s.[0]) 0xEF &&
-      Int.equal (Char.code s.[1]) 0xBB &&
-      Int.equal (Char.code s.[2]) 0xBF
-    in
-    let in_chan = open_in fname in
-    let s = "   " in
-    if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-    in_chan in
   let fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
-- 
cgit v1.2.3


From 86e2b0ab9da7dbd9c4c39ab2ab8df05d94a42056 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 13:42:30 +0200
Subject: Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").

Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
---
 tactics/term_dnet.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e79fc6dc9..65239a5f7 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -98,8 +98,8 @@ struct
   | DSort, DSort -> 0
   | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
-  | DLambda (tl1, tr1), DCtx (tl2, tr2)
-  | DApp (tl1, tr1), DCtx (tl2, tr2) ->
+  | DLambda (tl1, tr1), DLambda (tl2, tr2)
+  | DApp (tl1, tr1), DApp (tl2, tr2) ->
     let c = cmp tl1 tl2 in
     if c = 0 then cmp tr1 tr2 else c
 
-- 
cgit v1.2.3


From 3bdadb4020c1d3e51957a06c1e3a52744f09148d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 13:47:39 +0200
Subject: Tests for bugs #3509 and #3510.

---
 test-suite/bugs/closed/3509.v |  6 ++++++
 test-suite/bugs/closed/3510.v | 35 +++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3509.v | 19 -------------------
 test-suite/bugs/opened/3510.v | 35 -----------------------------------
 4 files changed, 41 insertions(+), 54 deletions(-)
 create mode 100644 test-suite/bugs/closed/3509.v
 create mode 100644 test-suite/bugs/closed/3510.v
 delete mode 100644 test-suite/bugs/opened/3509.v
 delete mode 100644 test-suite/bugs/opened/3510.v

diff --git a/test-suite/bugs/closed/3509.v b/test-suite/bugs/closed/3509.v
new file mode 100644
index 000000000..822662267
--- /dev/null
+++ b/test-suite/bugs/closed/3509.v
@@ -0,0 +1,6 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 : bar.
+Hint Rewrite a2 : bar.
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
new file mode 100644
index 000000000..daf265071
--- /dev/null
+++ b/test-suite/bugs/closed/3510.v
@@ -0,0 +1,35 @@
+Require Import TestSuite.admit.
+Lemma match_option_fn T (b : option T) A B s n
+: match b as b return forall x : A, B b x with
+    | Some k => s k
+    | None => n
+  end
+  = fun x : A => match b as b return B b x with
+                   | Some k => s k x
+                   | None => n x
+                 end.
+admit.
+Defined.
+Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
+: match p as p return R match p with
+                          | Some k => s1 k
+                          | None => n1
+                        end
+                        match p as p return B match p with Some k => s1 k | None => n1 end with
+                          | Some k => s2 k
+                          | None => n2
+                        end with
+    | Some k => f (s1 k) (s2 k)
+    | None => f n1 n2
+  end
+  = f match p return A with
+        | Some k => s1 k
+        | None => n1
+      end
+      match p as p return B match p with Some k => s1 k | None => n1 end with
+        | Some k => s2 k
+        | None => n2
+      end.
+admit.
+Defined.
+Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
deleted file mode 100644
index 3913bbb43..000000000
--- a/test-suite/bugs/opened/3509.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_bool_fn b A B xT xF
-: match b as b return forall x : A, B b x with
-    | true => xT
-    | false => xF
-  end
-  = fun x : A => match b as b return B b x with
-                   | true => xT x
-                   | false => xF x
-                 end.
-admit.
-Defined.
-Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
-: (if b as b return B (if b then t else f) then F t else F f)
-  = F (if b then t else f).
-admit.
-Defined.
-Hint Rewrite match_bool_fn : matchdb.
-Fail Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
deleted file mode 100644
index daf265071..000000000
--- a/test-suite/bugs/opened/3510.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
-- 
cgit v1.2.3


From 309907165909a08c4b6c2c05e87f458bb1873f91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 13:57:00 +0200
Subject: Updating test-suite for #3510.

---
 test-suite/bugs/closed/3510.v | 40 +++++-----------------------------------
 1 file changed, 5 insertions(+), 35 deletions(-)

diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
index daf265071..4cbae3359 100644
--- a/test-suite/bugs/closed/3510.v
+++ b/test-suite/bugs/closed/3510.v
@@ -1,35 +1,5 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 a2 : bar.
-- 
cgit v1.2.3


From 01248339f4f18cc1635b591447d343a1b4565a80 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Jul 2015 14:13:15 +0200
Subject: ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix
 #4308)

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1aaafd..de8752f41 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2451,7 +2451,7 @@ let get_script prf =
   let branch, test =
     match prf with
     | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),  List.mem name in
+    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
   let rec find acc id =
     if Stateid.equal id Stateid.initial ||
        Stateid.equal id Stateid.dummy then acc else
@@ -2462,7 +2462,9 @@ let get_script prf =
     | `Sideff (`Ast (x,_)) ->
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
     | `Sideff (`Id id)  -> find acc id
-    | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd _ -> find acc view.next
     | `Alias (id,_) -> find acc id
     | `Fork _ -> find acc view.next
     in
-- 
cgit v1.2.3


From e706bbd36237abc6c63d3e30cdaf9a42ac458215 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 15:10:35 +0200
Subject: Fixing bug #4281: Better escaping of XML attributes.

---
 lib/xml_lexer.mll  | 10 ++++++++++
 lib/xml_printer.ml |  2 ++
 2 files changed, 12 insertions(+)

diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index a33be9da7..f6943dd13 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -281,6 +281,11 @@ and dq_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         dq_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        dq_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
@@ -297,6 +302,11 @@ and q_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         q_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        q_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index eeddd53cb..bbb7b51ba 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) =
     match v.[p] with
       | '\\' -> output "\\\\"
       | '"' -> output "\\\""
+      | '<' -> output "&lt;"
+      | '&' -> output "&amp;"
       | c -> output' c
   done;
   output' '"'
-- 
cgit v1.2.3


From d0ec5640994fefe6674c5abb6f7c7001305073cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 28 Jul 2015 15:32:59 +0200
Subject: Reset a dangling proof in the FAQ.

---
 doc/faq/FAQ.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 8495156ca..b03aa6409 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -755,19 +755,19 @@ the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
  E.g. in this case (this occurs only in the {\tt Set}-impredicative
  variant of \Coq):
 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
 \begin{coq_example*}
 Inductive I : Type :=
   intro : forall k:Set, k -> I.
-Lemma eq_jdef : 
+Lemma eq_jdef :
    forall x y:nat, intro _ x = intro _ y -> x = y.
 Proof.
    intros x y H; injection H.
 \end{coq_example*}
 
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
  Injectivity of constructors is restricted to predicative types. If
 injectivity on large inductive types were not restricted, we would be
 allowed to derive an inconsistency (e.g. following the lines of
-- 
cgit v1.2.3


From c544167584024513648b23052db1aa9dcd993c01 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 28 Jul 2015 15:55:49 +0200
Subject: Make coq-tex aware of lines ending with "}", so as to fix the FAQ.

This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.

Example of crazy output:

Coq < Goal { True }
Coq < 1 subgoal

  ============================
   {True} + {False}

Coq <    + { False }.
---
 tools/coq_tex.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 7f2fe741e..fc652f584 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -68,7 +68,7 @@ let begin_coq_example =
 let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
 let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
 let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
+let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
 
 let has_match r s =
   try let _ = Str.search_forward r s 0 in true with Not_found -> false
-- 
cgit v1.2.3


From 0621891c4ba7606d91e614408378af17d3b0aee3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 17:00:20 +0200
Subject: Fix for bug #4280: "decide equality produces terms that don't compute
 well".

We postpone the rewriting of hypothesis until we actually commit to one
branch instead of doing it upfront.
---
 tactics/eqdecide.ml | 38 ++++++++++++++++++++++++++------------
 1 file changed, 26 insertions(+), 12 deletions(-)

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index a5d68e19b..4fb76bb82 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,22 +104,29 @@ let mkGenDecideEqGoal rectype g =
         (mkDecideEqGoal true (build_coq_sumbool ())
           rectype (mkVar xname) (mkVar yname))))
 
+let rec rewrite_and_clear hyps = match hyps with
+| [] -> Proofview.tclUNIT ()
+| id :: hyps ->
+  tclTHENLIST [
+    Equality.rewriteLR (mkVar id);
+    clear [id];
+    rewrite_and_clear hyps;
+  ]
+
 let eqCase tac =
-  (tclTHEN intro
-  (tclTHEN (onLastHyp Equality.rewriteLR)
-  (tclTHEN clear_last
-  tac)))
+  tclTHEN intro (onLastHypId tac)
 
-let diseqCase eqonleft =
+let diseqCase hyps eqonleft =
   let diseq  = Id.of_string "diseq" in
   let absurd = Id.of_string "absurd" in
   (tclTHEN (intro_using diseq)
   (tclTHEN (choose_noteq eqonleft)
+  (tclTHEN (rewrite_and_clear (List.rev hyps))
   (tclTHEN  (Proofview.V82.tactic red_in_concl)
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (Simple.apply (mkVar diseq))
   (tclTHEN  (Extratactics.injHyp absurd)
-            (full_trivial [])))))))
+            (full_trivial []))))))))
 
 open Proofview.Notations
 
@@ -131,15 +138,24 @@ let match_eqdec c =
 
 (* /spiwack *)
 
-let solveArg eqonleft op a1 a2 tac =
+let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+| [], [] ->
+  tclTHENLIST [
+    choose_eq eqonleft;
+    rewrite_and_clear (List.rev hyps);
+    intros_reflexivity;
+  ]
+| a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl a1 in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
+  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
   let subtacs =
-    if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
-    else [diseqCase eqonleft;eqCase tac;default_auto] in
+    if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
+    else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
   (tclTHENS (elim_type decide) subtacs)
   end
+| _ -> invalid_arg "List.fold_right2"
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
@@ -152,9 +168,7 @@ let solveEqBranch rectype =
           let getargs l = List.skipn nparams (snd (decompose_app l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
-          List.fold_right2
-            (solveArg eqonleft op) largs rargs
-            (tclTHEN (choose_eq eqonleft) intros_reflexivity)
+          solveArg [] eqonleft op largs rargs
       end
     end
     begin function (e, info) -> match e with
-- 
cgit v1.2.3


From 524bff66f40908dc3d17b6a18ee4253a2e61093e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Jul 2015 17:32:30 +0200
Subject: Adding a test for bug #4280.

---
 test-suite/bugs/closed/4280.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/4280.v

diff --git a/test-suite/bugs/closed/4280.v b/test-suite/bugs/closed/4280.v
new file mode 100644
index 000000000..fd7897509
--- /dev/null
+++ b/test-suite/bugs/closed/4280.v
@@ -0,0 +1,24 @@
+Require Import ZArith.
+Require Import Eqdep_dec.
+Local Open Scope Z_scope.
+
+Definition t := { n: Z | n > 1 }.
+
+Program Definition two : t := 2.
+Next Obligation. omega. Qed.
+
+Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
+  if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
+Next Obligation.
+  destruct x as [x Px], y as [y Py]. simpl in H; subst y.
+  f_equal. apply UIP_dec. decide equality.
+Qed.
+Next Obligation.
+  congruence.
+Qed.
+
+Definition t_list_eq: forall (x y: list t), {x=y} + {x<>y}.
+Proof. decide equality. apply t_eq. Defined.
+
+Goal match t_list_eq (two::nil) (two::nil) with left _ => True | right _ => False end.
+Proof. exact I. Qed.
-- 
cgit v1.2.3


From 97f33dd00718d49d2ba91eaba2de600d9e95b4d3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 29 Jul 2015 00:50:07 +0200
Subject: Fixing bug #3811: "Universe annotations confused inside generalizing
 binders".

The universe instance of the constant was simply dropped by the function
interpreting generalizing binders.
---
 interp/implicit_quantifiers.ml  | 16 ++++++++--------
 interp/implicit_quantifiers.mli |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e304725d4..87f7a6d6e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -245,21 +245,21 @@ let combine_params_freevar =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l
-    | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
+    | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let (loc, r, _ as clapp) = destClassAppExpl ty in
+      let (_, r, _, _ as clapp) = destClassAppExpl ty in
       let (loc, qid) = qualid_of_reference r in
       let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -267,7 +267,7 @@ let implicit_application env ?(allow_partial=true) f ty =
   in
     match is_class with
     | None -> ty, env
-    | Some ((loc, id, par), gr) ->
+    | Some ((loc, id, par, inst), gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
@@ -285,7 +285,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    CAppExpl (loc, (None, id, None), args), avoid
+	    CAppExpl (loc, (None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 818f7e9a8..a3721af66 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Globnames
 val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
-val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
-- 
cgit v1.2.3


From 0bc09220172b02c83eeba15350c26bd64cf0aa46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 27 Jul 2015 16:32:18 +0200
Subject: Fixing what seems to be a typo.

---
 proofs/pfedit.ml        |  2 +-
 proofs/proof_global.ml  | 10 +++++-----
 proofs/proof_global.mli |  2 +-
 stm/lemmas.ml           |  2 +-
 stm/stm.ml              |  4 ++--
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9c041d72c..d024c01ba 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -42,7 +42,7 @@ let cook_this_proof p =
 
 let cook_proof () =
   cook_this_proof (fst
-    (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
+    (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8677b854d..c02b90916 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -269,7 +269,7 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
@@ -290,7 +290,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
         let body = c and typ = nf t in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_sepatate then
+        if keep_body_ucst_separate then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
@@ -379,9 +379,9 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_sepatate fix_exn =
-  close_proof ~keep_body_ucst_sepatate ~now:true
+  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_separate fix_exn =
+  close_proof ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 88e047782..b5dd5ef85 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -91,7 +91,7 @@ val start_dependent_proof :
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
+val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index c766f3fab..6c8630404 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -503,7 +503,7 @@ let save_proof ?proof = function
       let (proof_obj,terminator) =
         match proof with
         | None ->
-            Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)
+            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
diff --git a/stm/stm.ml b/stm/stm.ml
index de8752f41..9e82dd156 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1220,7 +1220,7 @@ end = struct (* {{{ *)
         (Lemmas.standard_proof_terminator []
           (Lemmas.mk_hook (fun _ _ -> ())));
       let proof =
-        Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+        Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~cache:`No start;
@@ -1854,7 +1854,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                       qed.fproof <- Some (fp, ref false); None
                   | VtKeep ->
                       Some(Proof_global.close_proof
-                                ~keep_body_ucst_sepatate:false
+                                ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 reach view.next;
                 if keep == VtKeepAsAxiom then
-- 
cgit v1.2.3


From 0dac9618c695a345f82ee302b205217fff29be29 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 28 Jul 2015 10:18:08 +0200
Subject: Fixing some English misspelling.

---
 kernel/cbytegen.ml      | 22 +++++++++++-----------
 kernel/cemitcodes.ml    | 14 +++++++-------
 kernel/cemitcodes.mli   |  2 +-
 kernel/csymtable.ml     |  2 +-
 kernel/nativecode.ml    |  2 +-
 kernel/nativelambda.ml  |  6 +++---
 kernel/nativelambda.mli |  2 +-
 7 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d5435f0c3..3462694d6 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -524,14 +524,14 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env (kn,u as p) =
+let rec get_alias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     match tps with
     | None -> p
     | Some tps ->
        (match Cemitcodes.force tps with
-	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+	| BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u')
 	| _ -> p)
 
 (* Compiling expressions *)
@@ -756,10 +756,10 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_allias !global_env (kn, u)) :: cont
+      Kgetglobal (get_alias !global_env (kn, u)) :: cont
     else
       comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
+                   Kgetglobal (get_alias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
 let compile fail_on_error env c =
@@ -797,14 +797,14 @@ let compile_constant_body fail_on_error env = function
 	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      Some (BCallias (get_allias env (con,u)))
+	      Some (BCalias (get_alias env (con,u)))
 	| _ ->
 	    let res = compile fail_on_error env body in
 	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u)
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
@@ -867,7 +867,7 @@ let op2_compilation op =
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
-          (*Kgetglobal (get_allias !global_env kn):: *)
+          (*Kgetglobal (get_alias !global_env kn):: *)
           normal::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
      in
@@ -886,7 +886,7 @@ let op2_compilation op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = 2 and non-tailcall cont*)
-           (*Kgetglobal (get_allias !global_env kn):: *)
+           (*Kgetglobal (get_alias !global_env kn):: *)
            normal::
            Kapply 2::labeled_cont)))
   else if nargs=0 then
@@ -900,7 +900,7 @@ let op2_compilation op =
   1/ checks if all the arguments are constants (i.e. non-block values)
   2/ if they are, uses the "op" instruction to execute
   3/ if at least one is not, branches to the normal behavior:
-      Kgetglobal (get_allias !global_env kn) *)
+      Kgetglobal (get_alias !global_env kn) *)
 let op_compilation n op =
   let code_construct kn cont =
      let f_cont =
@@ -908,7 +908,7 @@ let op_compilation n op =
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          Kgetglobal (get_allias !global_env kn)::
+          Kgetglobal (get_alias !global_env kn)::
           Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
      in
      let lbl = Label.create () in
@@ -926,7 +926,7 @@ let op_compilation n op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = n and non-tailcall cont*)
-           Kgetglobal (get_allias !global_env kn)::
+           Kgetglobal (get_alias !global_env kn)::
            Kapply n::labeled_cont)))
   else if Int.equal nargs 0 then
     code_construct kn cont
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6dbfbe9cc..9b275cb6c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -328,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of pconstant
+  | BCalias of pconstant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of pconstant substituted
 | PBCconstant
 
 let from_val = function
 | BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
 | BCconstant -> PBCconstant
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_pconstant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
 | PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (subst_substituted s cu)
 | PBCconstant -> PBCconstant
 
 let repr_body_code = function
 | PBCdefined tp ->
   let (s, tp) = repr_substituted tp in
   (s, BCdefined tp)
-| PBCallias cu ->
+| PBCalias cu ->
   let (s, cu) = repr_substituted cu in
-  (s, BCallias cu)
+  (s, BCalias cu)
 | PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec901306..54b92b912 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant Univ.puniverses
+  | BCalias of constant Univ.puniverses
   | BCconstant
 
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8fd90ec36..b3f0ba5b5 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -163,7 +163,7 @@ let rec slot_for_getglobal env (kn,u) =
 	    let v = eval_to_patch env (code,pl,fv) in
 	      set_global v
 	    else set_global (val_of_constant (kn,u))
-	 | BCallias kn' -> slot_for_getglobal env kn'
+	 | BCalias kn' -> slot_for_getglobal env kn'
 	 | BCconstant -> set_global (val_of_constant (kn,u)) in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 90c437bbf..687b740f6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2012,7 +2012,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_allias env c in
+      let c,u = get_alias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 383f81029..cb08b5058 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,13 +373,13 @@ let makeblock env cn u tag args =
 
 (* Translation of constants *)
 
-let rec get_allias env (kn, u as p) =
+let rec get_alias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
     match tps with
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCallias kn' -> get_allias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env kn'
        | _ -> p
 
 (*i Global environment *)
@@ -651,7 +651,7 @@ let rec lambda_of_constr env sigma c =
 and lambda_of_app env sigma f args =
   match kind_of_term f with
   | Const (kn,u as c) ->
-      let kn,u = get_allias !global_env c in
+      let kn,u = get_alias !global_env c in
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ccf2888b5..3b6fafbbc 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -26,7 +26,7 @@ val mk_lazy : lambda -> lambda
 
 val get_mind_prefix : env -> mutual_inductive -> string
 
-val get_allias : env -> pconstant -> pconstant
+val get_alias : env -> pconstant -> pconstant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
 
-- 
cgit v1.2.3