From 1e3d73abd90af8646222bc4d6ea42f7d7ed3ddd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 23 Sep 2016 20:55:21 +0200
Subject: Fix bug #5096: [vm_compute] is exponentially slower than
 [native_compute].

The fix is essentially a revert of f22ad60 that introduced the use of the
pretyper version of whd_all instead of the one from the kernel. The exact
cause of slowness of the pretyper version is still to be investigated, but
it is believed that it is due to a call-by-name strategy, to compare with
call-by-need in the kernel.

Note that there is still something fishy in presence of evars. Technically
vm_compute does not handle them, but if this comes to be the case, it might
be worthwile to use an evar-aware variant of whd_all.
---
 pretyping/vnorm.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c396f593bb..e281f22df6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -46,7 +46,11 @@ let invert_tag cst tag reloc_tbl =
   with Find_at j -> (j+1)
              (* Argggg, ces constructeurs de ... qui commencent a 1*)
 
-let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c
+let find_rectype_a env c =
+  let (t, l) = decompose_appvect (whd_all env c) in
+  match kind_of_term t with
+  | Ind ind -> (ind, l)
+  | _ -> assert false
 
 (* Instantiate inductives and parameters in constructor type *)
 
-- 
cgit v1.2.3


From 8463f0a3f34aa1ca314bde1f3d19a3895df9dcaa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 Sep 2016 17:48:28 +0200
Subject: Adding a test for bug #5096.

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

diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v
new file mode 100644
index 0000000000..20a537ab3c
--- /dev/null
+++ b/test-suite/bugs/closed/5096.v
@@ -0,0 +1,219 @@
+Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
+
+Set Asymmetric Patterns.
+
+Notation eta x := (fst x, snd x).
+
+Inductive expr {var : Type} : Type :=
+| Const : expr
+| LetIn : expr -> (var -> expr) -> expr.
+
+Definition Expr := forall var, @expr var.
+
+Fixpoint count_binders (e : @expr unit) : nat :=
+match e with
+| LetIn _ eC => 1 + @count_binders (eC tt)
+| _ => 0
+end.
+
+Definition CountBinders (e : Expr) : nat := count_binders (e _).
+
+Class Context (Name : Type) (var : Type) :=
+  { ContextT : Type;
+    extendb : ContextT -> Name -> var -> ContextT;
+    empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _}, {_ _} _.
+Arguments extendb {_ _ _} _ _ _.
+Arguments empty {_ _ _}.
+
+Module Export Named.
+Inductive expr Name : Type :=
+| Const : expr Name
+| LetIn : Name -> expr Name -> expr Name -> expr Name.
+End Named.
+
+Global Arguments Const {_}.
+Global Arguments LetIn {_} _ _ _.
+
+Definition split_onames {Name : Type} (ls : list (option Name))
+  : option (Name) * list (option Name)
+  := match ls with
+          | cons n ls'
+            => (n, ls')
+          | nil => (None, nil)
+     end.
+
+Section internal.
+  Context (InName OutName : Type)
+          {InContext : Context InName (OutName)}
+          {ReverseContext : Context OutName (InName)}
+          (InName_beq : InName -> InName -> bool).
+
+  Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+           (e : expr InName) (new_names : list (option OutName))
+    : option (expr OutName)
+    := match e in Named.expr _ return option (expr _) with
+       | Const => Some Const
+       | LetIn n ex eC
+         => let '(n', new_names') := eta (split_onames new_names) in
+            match n', @register_reassign ctxi ctxr ex nil with
+            | Some n', Some x
+              => let ctxi := @extendb _ _ _ ctxi n n' in
+                 let ctxr := @extendb _ _ _ ctxr n' n in
+                 option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
+            | None, Some x
+              => let ctxi := ctxi in
+                 @register_reassign ctxi ctxr eC new_names'
+            | _, None => None
+            end
+       end.
+
+End internal.
+
+Global Instance pos_context (var : Type) : Context positive var
+  := { ContextT := PositiveMap.t var;
+       extendb ctx key v := PositiveMap.add key v ctx;
+       empty := PositiveMap.empty _ }.
+
+Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
+
+Section language5.
+  Context (Name : Type).
+
+  Local Notation expr := (@Top.expr Name).
+  Local Notation nexpr := (@Named.expr Name).
+
+  Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
+    : option (nexpr)
+    := match e in @Top.expr _ return option (nexpr) with
+       | Top.Const => Some Named.Const
+       | Top.LetIn ex eC
+         => match @ocompile ex nil, split_onames ls with
+            | Some x, (Some n, ls')%core
+              => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
+            | _, _ => None
+            end
+       end.
+
+  Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
+End language5.
+
+Global Arguments compile {_} e ls.
+
+Fixpoint merge_liveness (ls1 ls2 : list unit) :=
+  match ls1, ls2 with
+  | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
+  | nil, ls | ls, nil => ls
+  end.
+
+Section internal1.
+  Context (Name : Type)
+          (OutName : Type)
+          {Context : Context Name (list unit)}.
+
+  Definition compute_livenessf_step
+             (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
+             (ctx : Context)
+             (e : expr Name) (prefix : list unit)
+    : list unit
+    := match e with
+       | Const => prefix
+       | LetIn n ex eC
+         => let lx := @compute_livenessf ctx ex prefix in
+            let lx := merge_liveness lx (prefix ++ repeat tt 1) in
+            let ctx := @extendb _ _ _ ctx n (lx) in
+            @compute_livenessf ctx eC (prefix ++ repeat tt 1)
+       end.
+
+  Fixpoint compute_liveness ctx e prefix
+    := @compute_livenessf_step (@compute_liveness) ctx e prefix.
+
+  Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
+    : list (option OutName)
+    := match ls with
+       | nil => nil
+       | cons live xs
+         => match lsn with
+            | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
+            | nil => def :: @insert_dead_names_gen def xs nil
+            end
+       end.
+  Definition insert_dead_names def (e : expr Name)
+    := insert_dead_names_gen def (compute_liveness empty e nil).
+End internal1.
+
+Global Arguments insert_dead_names {_ _ _} def e lsn.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+
+Section language7.
+  Context {Context : Context unit (positive)}.
+
+  Local Notation nexpr := (@Named.expr unit).
+
+  Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
+    : option (nexpr)
+    := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
+       match e with
+       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
+                          (fun names => register_reassign empty empty e names)
+       | None => None
+       end.
+End language7.
+
+Global Arguments CompileAndEliminateDeadCode {_} e ls.
+
+Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
+  := {| ContextT := Ctx;
+        extendb ctx n v := extendb ctx (f n) v;
+        empty := empty |}.
+
+Definition Register := Datatypes.unit.
+
+Global Instance RegisterContext {var : Type} : Context Register var
+  := ContextOn (fun _ => 1%positive) (pos_context var).
+
+Definition syntax := Named.expr Register.
+
+Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
+  := match res return match res with None => _ | _ => _ end with
+     | Some v => v
+     | None => I
+     end.
+
+Definition dummy_registers (n : nat) : list Register
+  := List.map (fun _ => tt) (seq 0 n).
+Definition DefaultRegisters (e : Expr) : list Register
+  := dummy_registers (CountBinders e).
+
+Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
+
+Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@Top.Const var).
+
+Definition compiled_syntax : Expr := fun (var : Type) =>
+(
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+ @Top.Const var).
+
+Definition v :=
+  Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
+
+Timeout 2 Eval vm_compute in v.
-- 
cgit v1.2.3


From e6a054695a2f5d8be3f695975464f99571a69b75 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Sep 2016 19:20:23 +0200
Subject: Ensuring that the evar name is preserved by "rename" as it is already
 the case for clear and the conversion tactics.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a66dbd6e88..225ff3db94 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -335,7 +335,7 @@ let rename_hyp repl =
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
       Proofview.Refine.refine ~unsafe:true begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~store instance
+        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
       end
     end
 
-- 
cgit v1.2.3


From f487472a5628fdb43245e782b304705172a1f569 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Sep 2016 19:03:25 +0200
Subject: Moving "move" in the new proof engine.

---
 printing/printer.ml   |  3 ---
 proofs/logic.ml       | 14 +++++---------
 proofs/logic.mli      |  3 +++
 proofs/proof_type.mli |  1 -
 proofs/tacmach.ml     |  4 ----
 proofs/tacmach.mli    |  1 -
 tactics/tactics.ml    | 13 ++++++++++++-
 7 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 28fd92659e..6d54a5b3d5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -733,9 +733,6 @@ let pr_prim_rule = function
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
-  | Move (id1,id2) ->
-      (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
-
 (* Backwards compatibility *)
 
 let prterm = pr_lconstr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6f..e4c833627a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -276,6 +276,11 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
+let move_hyp_in_named_context hfrom hto sign =
+  let (left,right,declfrom,toleft) =
+    split_sign hfrom hto (named_context_of_val sign) in
+  move_hyp toleft (left,declfrom,right) hto
+
 (**********************************************************************)
 
 
@@ -549,12 +554,3 @@ let prim_refiner r sigma goal =
 	let sgl = List.rev sgl in
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
-
-    | Move (hfrom, hto) ->
-  	let (left,right,declfrom,toleft) =
-	  split_sign hfrom hto (named_context_of_val sign) in
-  	let hyps' =
-	  move_hyp toleft (left,declfrom,right) hto in
-	let (gl,ev,sigma) = mk_goal hyps' cl in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-  	  ([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2764d28c02..0dba9ef1ee 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -56,3 +56,6 @@ val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+  Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index f7798a0edb..c120796220 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,7 +22,6 @@ open Misctypes
 type prim_rule =
   | Cut of bool * bool * Id.t * types
   | Refine of constr
-  | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 50984c48e0..b9330ff007 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,15 +121,11 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-let move_hyp_no_check id1 id2 gl =
-  refiner (Move (id1,id2)) gl
-
 (* Versions with consistency checks *)
 
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 100ed1522e..727efcf6dc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,7 +92,6 @@ val refine_no_check           : constr -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8dfb526325..ce77df69f4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -313,7 +313,18 @@ let apply_clear_request clear_flag dft c =
   else Tacticals.New.tclIDTAC
 
 (* Moving hypotheses *)
-let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
+let move_hyp id dest =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let ty = Proofview.Goal.raw_concl gl in
+    let store = Proofview.Goal.extra gl in
+    let sign = named_context_val env in
+    let sign' = move_hyp_in_named_context id dest sign in
+    let env = reset_with_named_context sign' env in
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Evarutil.new_evar env sigma ~principal:true ~store ty
+    end }
+  end }
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
-- 
cgit v1.2.3


From 1ea09cb57dffd7cc9b6fa3ccec137ea3dfcc6980 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 Sep 2016 23:33:10 +0200
Subject: The coqtop options -Q and -R do not affect the ML loadpath anymore.

It seems that such options were adding the considered path to the ML loadpath
as well, which is not what is documented, and does not provide an atomic way
to manipulate Coq loadpaths.
---
 toplevel/coqinit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8a8dbe9601..acbf909cc6 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -108,7 +108,7 @@ let init_load_path () =
     (* additional loadpath, given with options -Q and -R *)
     List.iter
       (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
+        Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
-- 
cgit v1.2.3


From 2fa1dc39371b8f770ce662d56d85bf6f20413aac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Sep 2016 23:38:39 +0200
Subject: Fix bug #5090: Effect of -Q depends on coqtop's current directory.

This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It
seems that the original motivation was to deactivate a warning when overriding
the default loadpath binding of the current directory, but in the end it made
it non-overridable.
---
 library/loadpath.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/library/loadpath.ml b/library/loadpath.ml
index e6f6716c3d..d03c6c5553 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit =
     let replace =
       if DirPath.equal coq_path old_path then
         implicit <> old_implicit
-      else if DirPath.equal coq_path (Nameops.default_root_prefix)
-              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
-        false (* This is the default "-I ." path, don't override the old path *)
       else
         let () =
           (* Do not warn when overriding the default "-I ." path *)
-- 
cgit v1.2.3


From c8ca50f0cf961c9e31489f095463a99fc005c5de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 00:06:16 +0200
Subject: Fix bug #5093: typeclasses eauto depth arg does not accept a var.

---
 ltac/g_class.ml4              | 14 +++-----------
 test-suite/bugs/closed/5093.v | 11 +++++++++++
 2 files changed, 14 insertions(+), 11 deletions(-)
 create mode 100644 test-suite/bugs/closed/5093.v

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index eaa6aad4f6..18df596eb8 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
-let pr_depth _prc _prlc _prt = function
-    Some i -> Pp.int i
-  | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
-  | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
      set_typeclasses_debug d;
      set_typeclasses_depth depth
    ]
@@ -63,9 +55,9 @@ END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     [ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
      typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
 
diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v
new file mode 100644
index 0000000000..3ded4dd304
--- /dev/null
+++ b/test-suite/bugs/closed/5093.v
@@ -0,0 +1,11 @@
+Axiom P : nat -> Prop.
+Axiom PS : forall n, P n -> P (S n).
+Axiom P0 : P 0.
+
+Hint Resolve PS : foobar.
+Hint Resolve P0 : foobar.
+
+Goal P 100.
+Proof.
+Fail typeclasses eauto 100 with foobar.
+typeclasses eauto 101 with foobar.
-- 
cgit v1.2.3


From 3d9a1378adc3c7cd7a3013c80ea565792486b679 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 01:53:13 +0200
Subject: Partial fix for bug #5085: nsatz_compute stack overflows.

This fixes the stack overflow part of the bug, even if the tactic is still quite
slow. The offending functions have been written in a tail-recursive way.
---
 plugins/nsatz/ideal.ml | 44 ++++++++++++++++++++------------------------
 1 file changed, 20 insertions(+), 24 deletions(-)

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 482ce50538..1d74ee12bf 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -402,29 +402,25 @@ let polconst d c =
   [(c,m)]
 
 let plusP p q =
-  let rec plusP p q =
-    match p with
-      [] -> q
-    |t::p' -> 
-	match q with
-	  [] -> p
-	|t'::q' ->
-            match compare_mon (snd t) (snd t') with
-              1 -> t::(plusP p' q)
-            |(-1) -> t'::(plusP p q')
-            |_ -> let c=P.plusP (fst t) (fst t') in
-              match P.equal c coef0 with
-                true -> (plusP p' q')
-              |false -> (c,(snd t))::(plusP p' q')
-  in plusP p q
+  let rec plusP p q accu = match p, q with
+  | [], [] -> List.rev accu
+  | [], _ -> List.rev_append accu q
+  | _, [] -> List.rev_append accu p
+  | t :: p', t' :: q' ->
+    let c = compare_mon (snd t) (snd t') in
+    if c > 0 then plusP p' q (t :: accu)
+    else if c < 0 then plusP p q' (t' :: accu)
+    else
+      let c = P.plusP (fst t) (fst t') in
+      if P.equal c coef0 then plusP p' q' accu
+      else plusP p' q' ((c, (snd t)) :: accu)
+  in
+  plusP p q []
 
 (* multiplication by (a,monomial) *)
 let mult_t_pol a m p =
-  let rec mult_t_pol p =
-    match p with
-      [] -> []
-    |(b,m')::p -> ((P.multP a b),(mult_mon m m'))::(mult_t_pol p)
-  in mult_t_pol p
+  let map (b, m') = (P.multP a b, mult_mon m m') in
+  CList.map map p
 
 let coef_of_int x = P.of_num (Num.Int x)
 
@@ -451,11 +447,11 @@ let emultP a p =
   in emultP p
 
 let multP p q =
-  let rec aux p =
+  let rec aux p accu =
     match p with
-      [] -> []
-    |(a,m)::p' -> plusP (mult_t_pol a m q) (aux p')
-  in aux p
+      [] -> accu
+    |(a,m)::p' -> aux p' (plusP (mult_t_pol a m q) accu)
+  in aux p []
 
 let puisP p n=
   match p with
-- 
cgit v1.2.3


From ad56f07611f78abb612e8c8c22866ea45040f11e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 02:02:54 +0200
Subject: Monomorphizing various uses of arrays in Nsatz.

---
 plugins/nsatz/ideal.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 1d74ee12bf..67355ccc37 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -127,11 +127,11 @@ type polynom =
     num : int;
     sugar : int}
 
-let nvar m =  Array.length m - 1
+let nvar (m : mon) =  Array.length m - 1
 
-let deg m = m.(0)
+let deg (m : mon) = m.(0)
 
-let mult_mon m m' =
+let mult_mon (m : mon) (m' : mon) =
   let d = nvar m in
   let m'' = Array.make (d+1) 0 in
   for i=0 to d do
@@ -140,7 +140,7 @@ let mult_mon m m' =
   m''
 
 
-let compare_mon m m' =
+let compare_mon (m : mon) (m' : mon) =
   let d = nvar m in
   if !lexico
   then (
@@ -148,18 +148,18 @@ let compare_mon m m' =
     let res=ref 0 in
     let i=ref 1 in (* 1 si lexico pur 0 si degre*)
     while (!res=0) && (!i<=d) do
-      res:= (compare m.(!i) m'.(!i));
+      res:= (Int.compare m.(!i) m'.(!i));
       i:=!i+1;
     done;
     !res)
   else (
      (* degre lexicographique inverse *)
-    match compare m.(0) m'.(0) with
+    match Int.compare m.(0) m'.(0) with
     | 0 -> (* meme degre total *)
 	let res=ref 0 in
 	let i=ref d in
 	while (!res=0) && (!i>=1) do
-	  res:= - (compare m.(!i) m'.(!i));
+	  res:= - (Int.compare m.(!i) m'.(!i));
 	  i:=!i-1;
 	done;
 	!res
-- 
cgit v1.2.3


From 5d36de8e2304661e76ac433d5dd90c13b3b86c72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 02:30:45 +0200
Subject: Fast russian peasant exponentiation in Nsatz.

---
 plugins/nsatz/ideal.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 67355ccc37..7c2178222f 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -457,13 +457,17 @@ let puisP p n=
   match p with
     [] -> []
   |_ ->
+    if n = 0 then
       let d = nvar (snd (List.hd p)) in
-      let rec puisP n =
-	match n with
-	  0 -> [coef1, Array.make (d+1) 0]
-	| 1 -> p
-	|_ -> multP p (puisP (n-1))
-      in puisP n
+      [coef1, Array.make (d+1) 0]
+    else
+      let rec puisP p n =
+        if n = 1 then p
+        else
+          let q = puisP p (n / 2) in
+          let q = multP q q in
+          if n mod 2 = 0 then q else multP p q
+      in puisP p n
 	
 let rec contentP p =
   match p with
-- 
cgit v1.2.3


From 980b434552d73cb990860f8d659b64686f6dbc87 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 18 Aug 2016 13:24:50 +0200
Subject: Inference of return clause: giving uniformly priority to "small
 inversion".

As noted by Jason Gross on coq-club (Aug 18, 2016), the "small
inversion" heuristic is not used consistently depending on whether the
variables in the type constraint are Rel or Var.

This commit simply gives uniformly preference to the inversion of the
predicate along the indices of the type over other heuristics.

The next three commits will improve further a uniform use of the
different heuristics.

----------------------------------------------------------------------
Here are some extra comments on how to go further with the inference
of the return predicate:

The "small inversion" heuristic build_inversion_problem (1) is
characterized by two features:

- small inversion properly speaking (a), i.e. that is for a match on
  t:I params p1(u11..u1p1) ... pn(un1..unpn) with pi exposing the
  constructor structure of the indices of the type of t, a return
  clause of the form "fun x1..xn (y:I params x1..xn) => match x1..xn y with
  | p1(z11..z1p1) ... pn(zn1..znpn) => ?T@{z11..znpn}
  | _ => IDProp
  end" is used,

- the dependent subterms in the external type constraint U are replaced
  by existential variables (b) which can be filled either by projecting
  (i.e. installing a dependency) or imitating (i.e. no dependency);
  this is obtained by solving the constraint ?T@{u11..unpn} == U by
  setting ?T@{z11..znpn} := U'(...?wij@{zij:=uij}...) where U has been
  written under the form U'(...uij...) highlighting all occurrences of
  each of the uij occurring in U; otherwise said the problem is reduced to
  the question of instantiating each wij, deciding whether wij@{zij} := zij
  (projection) or wij@{zij} := uij (imitation) [There may be different
  way to expose the uij in U, e.g. in the presence of overlapping, or of
  evars in U; this is left undetermined].

The two other heuristics used are:

- prepare_predicate_from_arsign_tycon (2): takes the external type
  constraint U and decides that each subterm of the form xi or y for a
  match on "y:I params x1 ... xn" is dependent; otherwise said, it
  corresponds to the degenerated form of (1) where
  - no constructor structure is exposed (i.e. each pi is trivial)
  - only uij that are Rel are replaced by an evar ?wij and this evar is
    directly instantiated by projection (hence creating a dependency),

- simple use of of an evar in case no type constraint is given (3):
  this evar is not dependent on the indices nor on the term to match.

Heuristic (1) is not strictly more powerful than other heuristics
because of (at least) two weaknesses.

- The first weakness is due to feature (b), i.e. to letting
  unification decide whether these evars have to create a dependency
  (projection) or not (imitation).

  In particular, the heuristic (2) gives priority to systematic
  abstraction over the dependencies (i.e. giving priority to
  projection over imitation) and it can then be better as the
  following example (from RelationClasses.v) shows:

  Fixpoint arrows (l : Tlist) (r : Type) : Type :=
    match l with
    | Tnil => r
    | A :: l' => A -> arrows l' r
    end.

  Fixpoint predicate_all (l : Tlist) : arrows l Prop -> Prop :=
    match l with
    | Tnil => fun f => f
    | A :: tl => fun f => forall x : A, predicate_all tl (f x)
    end.

  Using (1) fails. It proposes the predicate
  "fun l' => arrows ?l[l':=l'] Prop" so that typing the first branch
  leads to unify "arrows ?l[l:=Tnil] Prop == Prop", a problem about
  which evarconv unification is not able (yet!) to see what are the
  two possible solutions. Using (2) works. It instead directly
  suggests that the predicate is "fun l => arrows l Prop" is used, so
  that unification is not needed.

  Even if in practice the (2) is good (and hence could be added to
  (1)), it is not universally better. Consider e.g.

     y:bool,H1:P y,H2:P y,f:forall y, P y -> Q y |-
              match y as z return Q y with
              | true  => f y H1
              | false => f y H2
              end : Q y

  There is no way to type it with clause "as z return Q z" even if
  trying to generalize H1 and H2 so that they get type P z.

- A second weakness is due to the interaction between small inversion
  and constructors having a type whose indices havex a less refined
  constructor structure than in the term to match, as in:

  Inductive I : nat -> Set :=
  | C1 : forall n : nat, listn n -> I n
  | C2 : forall n : nat, I n -> I n.

  Check (fun x : I 0 => match x with
                        | C1 n l => 0
                        | C2 n c => 0
                        end).

  where the inverted predicate is "in I n return match n with 0 => ?T | _ => IDProp end"
  but neither C1 nor C2 have fine enough types so that n becomes
  constructed. There is a generic solution to that kind of situation which
  is to compile the above into

  Check (fun x : I 0 => match x with
                        | C1 n l => match n with 0 => 0 | _ -> id end
                        | C2 n c => match n with 0 => 0 | _ -> id end
                        end).

  but this is not implemented yet.

  In the absence of this refinement, heuristic (3) can here work
  better.

So, the current status of the claim is that for (1) to be strictly
more powerful than other current heuristics, work has to be done

- (A) at the unification level (by either being able to reduce problems of
  the form "match ?x[constructor] with ... end = a-rigid-term", or, at
  worst, by being able to use the heuristic favoring projecting for such
  a problem), so that it is better than (2),

- (B) at the match compilation level, by enforcing that, in each branch,
  the corresponding constructor is refined so has to match (or
  discriminate) the constraints given by the type of the term to
  match, and hence being better than (3).

Moreover, (2) and (3) are disjoint. Here is an example which (3) can
solve but not (2) (and (1) cannot because of (B)). [To be fixed in
next commit.]

Inductive I : bool -> bool -> Type := C : I true true | D x : I x x.

Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
              match y with
              | C  => f y H1
              | D _ => f y H2
              end : Q y z.

Indeed, (2) infers "as y' in I b z return Q y z" which does not work.

Here is an example which (2) can solve but not (3) (and (1) cannot
because of (B) again). [To be fixed in 2nd next commit].

Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
              match y with
              | C  => f y true H1
              | D b => f y b H2
              end : Q y z.
---
 pretyping/cases.ml | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fe2b0a5a1a..9d461d1aa1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1925,10 +1925,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * type and 1 assumption for each term not _syntactically_ in an
  * inductive type.
 
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: we try to specialize the
- * tycon to make the predicate if it is not closed.
+ * Each matched term is independently considered dependent or not.
  *)
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
@@ -1938,14 +1935,14 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
     | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
+	(* First strategy: we build an "inversion" predicate *)
+	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
+        let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
-	(* Second strategy: we build an "inversion" predicate *)
-	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	(match p1 with
-	 | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
-	 | None -> [sigma2, pred2])
+	(match p2 with
+	 | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
+	 | None -> [sigma1, pred1])
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -1960,7 +1957,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we directly use the evar as a non dependent pred *)
+	(* Second strategy: we use the evar or tycon as a non dependent pred *)
         let pred2 = lift (List.length (List.flatten arsign)) t in
 	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
-- 
cgit v1.2.3


From 2422aeb2b59229891508f35890653a9737988c00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 16:52:12 +0200
Subject: Trying a no-inversion no-dependency heuristic for match return
 clause.

The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.

See previous commit for discussion.
---
 pretyping/cases.ml          | 41 ++++++++++++++++++++++-------------------
 test-suite/success/Case13.v | 14 ++++++++++++++
 2 files changed, 36 insertions(+), 19 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9d461d1aa1..464dc18b95 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1932,32 +1932,35 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No return clause *)
-    | None, Some t when not (noccur_with_meta 0 max_int t) ->
-	(* If the tycon is not closed w.r.t real variables, we try *)
-        (* two different strategies *)
-	(* First strategy: we build an "inversion" predicate *)
+    | None, Some t ->
+        (* First strategy: we build an "inversion" predicate, also replacing the *)
+        (* dependencies with existential variables *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+        (* Third strategy: we take the type constraint as it is; of course we could *)
+        (* need something inbetween, abstracting some but not all of the dependencies *)
+        (* the "inversion" strategy deals with that but unification may not be *)
+        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
+        (* work (yet) when a constructor has a type not precise enough for the inversion *)
+        (* see log message for details *)
+        let pred3 = lift (List.length (List.flatten arsign)) t in
 	(match p2 with
-	 | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
-	 | None -> [sigma1, pred1])
-    | None, _ ->
-	(* No dependent type constraint, or no constraints at all: *)
-	(* we use two strategies *)
-        let sigma,t = match tycon with
-	| Some t -> sigma,t
-	| None -> 
-          let sigma = Sigma.Unsafe.of_evar_map sigma in
-          let Sigma ((t, _), sigma, _) =
-	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
-          let sigma = Sigma.to_evar_map sigma in
-	    sigma, t
-	in
+	 | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
+             [sigma1, pred1; sigma2, pred2; sigma, pred3]
+	 | _ ->
+             [sigma1, pred1; sigma, pred3])
+    | None, None ->
+        (* No type constraint: we use two strategies *)
+        (* we first create a generic evar type constraint *)
+        let src = (loc, Evar_kinds.CasesType false) in
+        let sigma = Sigma.Unsafe.of_evar_map sigma in
+        let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
+        let sigma = Sigma.to_evar_map sigma in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we use the evar or tycon as a non dependent pred *)
+	(* Second strategy: we use the evar as a non dependent pred *)
         let pred2 = lift (List.length (List.flatten arsign)) t in
 	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..e388acdcb0 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,17 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
-- 
cgit v1.2.3


From 292f365185b7acdee79f3ff7b158551c2764c548 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:13:58 +0200
Subject: Trying an abstracting dependencies heuristic for the match return
 clause even when no type constraint is given.

This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.

By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.

See penultimate commit for discussion.
---
 pretyping/cases.ml          | 28 +++++++++++++---------------
 test-suite/success/Case13.v | 12 ++++++++++++
 2 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 464dc18b95..1b1f958838 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1930,9 +1930,19 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
-    match pred, tycon with
+    match pred with
     (* No return clause *)
-    | None, Some t ->
+    | None ->
+        let sigma,t =
+          match tycon with
+          | Some t -> sigma, t
+          | None ->
+             (* No type constraint: we first create a generic evar type constraint *)
+             let src = (loc, Evar_kinds.CasesType false) in
+             let sigma = Sigma.Unsafe.of_evar_map sigma in
+             let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
+             let sigma = Sigma.to_evar_map sigma in
+             sigma, t in
         (* First strategy: we build an "inversion" predicate, also replacing the *)
         (* dependencies with existential variables *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
@@ -1951,20 +1961,8 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
              [sigma1, pred1; sigma2, pred2; sigma, pred3]
 	 | _ ->
              [sigma1, pred1; sigma, pred3])
-    | None, None ->
-        (* No type constraint: we use two strategies *)
-        (* we first create a generic evar type constraint *)
-        let src = (loc, Evar_kinds.CasesType false) in
-        let sigma = Sigma.Unsafe.of_evar_map sigma in
-        let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
-        let sigma = Sigma.to_evar_map sigma in
-        (* First strategy: we build an "inversion" predicate *)
-	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
-	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
-    | Some rtntyp, _ ->
+    | Some rtntyp ->
       (* We extract the signature of the arity *)
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index e388acdcb0..8fad41cd8f 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -101,3 +101,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
         | F  => f y H1
         | G _ => f y H2
         end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
-- 
cgit v1.2.3


From 0658ba7b908dad946200f872f44260d0e4893a94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:29:26 +0200
Subject: Posssible abstractions over goal variables when inferring match
 return clause.

The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".

By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".

See antepenultimate commit for discussion.
---
 pretyping/cases.ml          | 36 +++++++++++++++++++++++++-----------
 test-suite/success/Case13.v | 12 ++++++++++++
 2 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1b1f958838..e89c3ea719 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,16 +1870,22 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
+let add_subst c len (rel_subst,var_subst) =
+  match kind_of_term c with
+  | Rel n -> (n,len) :: rel_subst, var_subst
+  | Var id -> rel_subst, (id,len) :: var_subst
+  | _ -> assert false
+
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let subst, len =
+  let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel n when dependent tm c
+	  | Rel _ | Var _ when dependent tm c
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
+	      (add_subst tm len subst, len - signlen)
+	  | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1888,28 +1894,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel n when dependent arg c ->
-			      ((n, len) :: subst, pred len)
+			  | Rel _ | Var _ when dependent arg c ->
+			      (add_subst arg len subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
-		      then (n, len) :: subst else subst
+		      if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
+		      then add_subst tm len subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign ([], nar)
+      (List.rev tomatchs) arsign (([],[]), nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) subst in
+	      let idx = Int.List.assoc (n - lift) rel_subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
+	      (* A variable that is not matched, lift over the arsign *)
 	      mkRel (n + nar))
+      | Var id ->
+	  (try
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = Id.List.assoc id var_subst in
+		mkRel (idx + lift)
+	    with Not_found ->
+	      (* A variable that is not matched *)
+	      c)
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8fad41cd8f..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -113,3 +113,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
         | F  => f y true H1
         | G b => f y b H2
         end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.
-- 
cgit v1.2.3


From 7bc04ff2cc9d511c4b8552a3e5f9ad416917fb95 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 11 Jun 2016 17:23:08 -0400
Subject: Fix bug #4785 (use [ ] for vector nil)

Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
---
 test-suite/bugs/closed/4785.v | 26 ++++++++++++++++++++++++++
 theories/Compat/Coq85.v       | 21 ++++++++++++++++++++-
 theories/Vectors/VectorDef.v  |  7 ++++---
 3 files changed, 50 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/4785.v

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 0000000000..b844af68a9
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,26 @@
+Require Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Require Import Coq.Compat.Coq85.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 0ddf1acdea..6e495b05c6 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -21,4 +21,23 @@ Global Unset Regular Subst Tactic.
 Global Unset Structural Injection.
 Global Unset Shrink Abstract.
 Global Unset Shrink Obligations.
-Global Set Refolding Reduction.
\ No newline at end of file
+Global Set Refolding Reduction.
+
+(** In Coq 8.5, [] meant Vector, and [ ] meant list.  Restore this
+    behavior, to allow user-defined [] to not override vector
+    notations.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *)
+
+Require Coq.Lists.List.
+Require Coq.Vectors.VectorDef.
+Module Export Coq.
+Module Export Vectors.
+Module VectorDef.
+Module VectorNotations.
+Export Coq.Vectors.VectorDef.VectorNotations.
+Notation "[]" := (VectorDef.nil _) : vector_scope.
+End VectorNotations.
+End VectorDef.
+End Vectors.
+End Coq.
+Export Vectors.VectorDef.VectorNotations.
+Close Scope vector_scope. (* vector_scope is not opened by default *)
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index c692238041..095cda398d 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -30,7 +30,7 @@ Inductive t A : nat -> Type :=
   |nil : t A 0
   |cons : forall (h:A) (n:nat), t A n -> t A (S n).
 
-Local Notation "[]" := (nil _).
+Local Notation " [ ] " := (nil _) (format "[ ]").
 Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
 
 Section SCHEMES.
@@ -102,7 +102,7 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 
 Computational behavior of this function should be the same as
 ocaml function. *)
-Definition nth {A} := 
+Definition nth {A} :=
 fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
  |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
@@ -293,7 +293,8 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni
 End VECTORLIST.
 
 Module VectorNotations.
-Notation "[]" := [] : vector_scope.
+Delimit Scope vector_scope with vector.
+Notation " [ ] " := [] (format "[ ]") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
 Notation " [ x ] " := (x :: []) : vector_scope.
-- 
cgit v1.2.3


From f8745b1dbc87a8fee4943a91f517dc2afcd7804b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 11 Jun 2016 18:09:01 -0400
Subject: Unbreak Ltac [ | .. | ] notation in -compat 8.5

Importing VectorNotations breaks `; []`.  So we make sure it's not
imported by defualt.  Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
---
 test-suite/bugs/closed/4785.v | 23 +++++++++++++++++++++--
 theories/Compat/Coq85.v       |  3 +--
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index b844af68a9..14af2d91df 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -1,4 +1,8 @@
-Require Import Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+Import Coq.Lists.List Coq.Vectors.Vector.
 Import ListNotations.
 Check [ ]%list : list _.
 Import VectorNotations ListNotations.
@@ -8,6 +12,10 @@ Check []%vector : Vector.t _ _.
 Check [ ]%list : list _.
 Check []%list : list _.
 
+Goal True.
+  idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
+Abort.
+
 Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
 Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
@@ -18,9 +26,20 @@ Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
 Notation " [ x ] " := (mycons x nil) : mylist_scope.
 Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
 
-Require Import Coq.Compat.Coq85.
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
 
 Check []%vector : Vector.t _ _.
 Check []%mylist : mylist _.
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 6e495b05c6..54aeeaa114 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -32,6 +32,7 @@ Require Coq.Vectors.VectorDef.
 Module Export Coq.
 Module Export Vectors.
 Module VectorDef.
+Export Coq.Vectors.VectorDef.
 Module VectorNotations.
 Export Coq.Vectors.VectorDef.VectorNotations.
 Notation "[]" := (VectorDef.nil _) : vector_scope.
@@ -39,5 +40,3 @@ End VectorNotations.
 End VectorDef.
 End Vectors.
 End Coq.
-Export Vectors.VectorDef.VectorNotations.
-Close Scope vector_scope. (* vector_scope is not opened by default *)
-- 
cgit v1.2.3


From 53ac7ca0cd74b62d47472c0dabfcc8dc1cacd86c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 26 Sep 2016 13:11:03 -0400
Subject: Remove spaces from around vector notations

---
 theories/Vectors/VectorDef.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 095cda398d..f49b340758 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -30,7 +30,7 @@ Inductive t A : nat -> Type :=
   |nil : t A 0
   |cons : forall (h:A) (n:nat), t A n -> t A (S n).
 
-Local Notation " [ ] " := (nil _) (format "[ ]").
+Local Notation "[ ]" := (nil _) (format "[ ]").
 Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
 
 Section SCHEMES.
@@ -294,11 +294,11 @@ End VECTORLIST.
 
 Module VectorNotations.
 Delimit Scope vector_scope with vector.
-Notation " [ ] " := [] (format "[ ]") : vector_scope.
+Notation "[ ]" := [] (format "[ ]") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
-Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; y ; .. ; z ] " := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
+Notation "[ x ]" := (x :: []) : vector_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
 .
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
-- 
cgit v1.2.3


From b04a1d6eb82f24844bfc0a07ab0801d3a4169c6b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 26 Sep 2016 13:20:07 -0400
Subject: Remove spaces from around list notations

---
 theories/Compat/Coq84.v |  4 ++--
 theories/Lists/List.v   | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 341be92d1d..5eecdc64cc 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -77,8 +77,8 @@ Coercion sig2_of_sigT2 : sigT2 >-> sig2.
 (** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5.  This is necessary.  These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *)
 Require Coq.Lists.List.
 Require Coq.Vectors.VectorDef.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
-Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope.
+Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
 
 (** In 8.4, the statement of admitted lemmas did not depend on the section
     variables. *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 9886ae6a8e..fc94d7e254 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -21,12 +21,12 @@ Set Implicit Arguments.
 
 Open Scope list_scope.
 
-(** Standard notations for lists. 
+(** Standard notations for lists.
 In a special module to avoid conflicts. *)
 Module ListNotations.
-Notation " [ ] " := nil (format "[ ]") : list_scope.
-Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; y ; .. ; z ] " :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
+Notation "[ ]" := nil (format "[ ]") : list_scope.
+Notation "[ x ]" := (cons x nil) : list_scope.
+Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
 End ListNotations.
 
 Import ListNotations.
@@ -195,7 +195,7 @@ Section Facts.
   Qed.
 
   Theorem app_nil_r : forall l:list A, l ++ [] = l.
-  Proof. 
+  Proof.
     induction l; simpl; f_equal; auto.
   Qed.
 
-- 
cgit v1.2.3


From 160a6d8806516b40d6406ebe0ae6c0240e969d85 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 27 Sep 2016 07:46:04 +0200
Subject: LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)

It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.
---
 ltac/profile_ltac.ml          | 17 ++++++++++-------
 ltac/profile_ltac.mli         |  3 ++-
 ltac/profile_ltac_tactics.ml4 |  3 ++-
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index fe591c7756..102918e5e5 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -166,7 +166,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
 and print_table ~filter all_total indent first_level table =
   let fold _ n l =
     let s, total = n.name, n.total in
-    if filter s then (s, n) :: l else l in
+    if filter s total then (s, n) :: l else l in
   let ls = M.fold fold table [] in
   match ls with
   | [s, n] when not first_level ->
@@ -182,7 +182,7 @@ and print_table ~filter all_total indent first_level table =
     in
     prlist (fun pr -> pr) (list_iter_is_last iter ls)
 
-let to_string ~filter node =
+let to_string ~filter ?(cutoff=0.0) node =
   let tree = node.children in
   let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
   let flat_tree =
@@ -218,6 +218,7 @@ let to_string ~filter node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
+  let filter s n = filter s && n >= cutoff in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
@@ -387,22 +388,24 @@ let reset_profile () =
 
 (* ******************** *)
 
-let print_results_filter ~filter =
+let print_results_filter ~cutoff ~filter =
   let valid id _ = Stm.state_of_id id <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
-let print_results () = print_results_filter ~filter:(fun _ -> true)
+let print_results ~cutoff =
+  print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~filter:(fun s ->
+  print_results_filter ~cutoff:0.0 ~filter:(fun s ->
     String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
 
-let do_print_results_at_close () = if get_profiling () then print_results ()
+let do_print_results_at_close () =
+  if get_profiling () then print_results ~cutoff:0.0
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8c4b47b8e4..e5e2e41975 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -14,7 +14,8 @@ val do_profile :
 
 val set_profiling : bool -> unit
 
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
 
 val print_results_tactic : string -> unit
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb61..9083bda60a 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-  [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
-- 
cgit v1.2.3