Merge remote-tracking branch 'gforge/v8.5' into v8.6

7 files changed, 186 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index b4e98a0b1..b2113e0bf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -85,7 +85,16 @@ Tools
 
 Changes from V8.5pl2 to V8.5pl3
 ===============================
+
+Critical bugfix
+- #4876: Guard checker incompleteness when using primitive projections
+
+Other bugfixes
+
 - #4780: Induction with universe polymorphism on was creating ill-typed terms.
+- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
+- #4769: Anomaly with universe polymorphic schemes defined inside sections.
+- #3886: Program: duplicate obligations of mutual fixpoints
 
 Changes from V8.5pl1 to V8.5pl2
 ===============================
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index e327deda0..df96cfcf6 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -438,14 +438,22 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
+let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
+  pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+
+let problem_inclusion x y =
+  List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
+
 let evd_convertible env evd x y =
   try
-    let evd = Evarconv.the_conv_x env x y evd in
     (* Unfortunately, the_conv_x might say they are unifiable even if some
-        unsolvable constraints remain, so we check them here *)
-    let evd = Evarconv.consider_remaining_unif_problems env evd in
-    let () = Evarconv.check_problems_are_solved env evd in
-    Some evd
+       unsolvable constraints remain, so we check that this unification
+       does not introduce any new problem. *)
+    let _, pbs = Evd.extract_all_conv_pbs evd in
+    let evd' = Evarconv.the_conv_x env x y evd in
+    let _, pbs' = Evd.extract_all_conv_pbs evd' in
+    if evd' == evd || problem_inclusion pbs' pbs then Some evd'
+    else None
   with e when CErrors.noncritical e -> None
 
 let convertible env evd x y =
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 99c2d8210..93073fdc7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -52,19 +52,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
-    let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+    let sigma = Evd.merge_universe_context sigma ectx in
+    let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
       (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
+  let sigma = Evd.from_env env in
   let ctx = 
     let mib,mip = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_context mib
   in
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
-  let ectx = Evd.evar_universe_context_of ctxset in
-  let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+  let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
+  let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v
new file mode 100644
index 000000000..2ac4abe54
--- /dev/null
+++ b/test-suite/bugs/closed/3886.v
@@ -0,0 +1,23 @@
+Require Import Program.
+
+Inductive Even : nat -> Prop :=
+| evenO : Even O
+| evenS : forall n, Odd n -> Even (S n)
+with Odd : nat -> Prop :=
+| oddS : forall n, Even n -> Odd (S n).
+
+Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n)
+  := _
+with doubleO {n} (o : Odd n) : Odd (S (2 * n))
+     := _.
+Obligations.
+Axiom cheat : forall {A}, A.
+Obligation 1 of doubleE.
+apply cheat.
+Qed.
+
+Obligation 1 of doubleO.
+apply cheat.
+Qed.
+
+Check doubleE.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v
new file mode 100644
index 000000000..5bb3cd1be
--- /dev/null
+++ b/test-suite/bugs/closed/4754.v
@@ -0,0 +1,35 @@
+
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
+Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  setoid_rewrite (FG _ _); [ | reflexivity.. ].
+  Undo.
+  setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v
new file mode 100644
index 000000000..d87906f31
--- /dev/null
+++ b/test-suite/bugs/closed/4769.v
@@ -0,0 +1,94 @@
+
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3
+   coqtop version trunk (June 2016) *)
+
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x * y" (at level 40, left associativity).
+Delimit Scope type_scope with type.
+Open Scope type_scope.
+Global Set Universe Polymorphism.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Set Implicit Arguments.
+Global Set Nonrecursive Elimination Schemes.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Axiom admit : forall {T}, T.
+Delimit Scope function_scope with function.
+Notation compose := (fun g f x => g (f x)).
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+Record PreCategory :=
+  Build_PreCategory {
+      object :> Type;
+      morphism : object -> object -> Type;
+      identity : forall x, morphism x x }.
+Bind Scope category_scope with PreCategory.
+Record Functor (C D : PreCategory) := { object_of :> C -> D }.
+Bind Scope functor_scope with Functor.
+Class Isomorphic {C : PreCategory} (s d : C) := {}.
+Definition oppositeC (C : PreCategory) : PreCategory
+  := @Build_PreCategory C (fun s d => morphism C d s) admit.
+Notation "C ^op" := (oppositeC C) (at level 3, format "C '^op'") : category_scope.
+Definition oppositeF C D (F : Functor C D) : Functor C^op D^op
+  := Build_Functor (C^op) (D^op) (object_of F).
+Definition set_cat : PreCategory := @Build_PreCategory Type (fun x y => x -> y) admit.
+Definition prodC (C D : PreCategory) : PreCategory
+  := @Build_PreCategory
+       (C * D)%type
+       (fun s d => (morphism C (fst s) (fst d)
+                    * morphism D (snd s) (snd d))%type)
+       admit.
+Infix "*" := prodC : category_scope.
+Section composition.
+  Variables B C D E : PreCategory.
+  Definition composeF (G : Functor D E) (F : Functor C D) : Functor C E := Build_Functor C E (fun c => G (F c)).
+End composition.
+Infix "o" := composeF : functor_scope.
+Definition fstF {C D} : Functor (C * D) C := admit.
+Definition sndF {C D} : Functor (C * D) D := admit.
+Definition prodF C D D' (F : Functor C D) (F' : Functor C D') : Functor C (D * D') := admit.
+Local Infix "*" := prodF : functor_scope.
+Definition pairF C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D')
+  := (F o fstF) * (F' o sndF).
+Section hom_functor.
+  Variable C : PreCategory.
+  Local Notation obj_of c'c :=
+    ((morphism
+        C
+        (fst (c'c : object (C^op * C)))
+        (snd (c'c : object (C^op * C))))).
+  Definition hom_functor : Functor (C^op * C) set_cat
+    := Build_Functor (C^op * C) set_cat (fun c'c => obj_of c'c).
+End hom_functor.
+Definition identityF C : Functor C C := admit.
+Definition functor_category (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (Functor C D) admit admit.
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G.
+
+Section Adjunction.
+  Variables C D : PreCategory.
+  Variable F : Functor C D.
+  Variable G : Functor D C.
+  
+  Record AdjunctionHom :=
+    {
+      mate_of : @NaturalIsomorphism
+                  (prodC (oppositeC C) D)
+                  (@set_cat)
+                  (@composeF
+                     (prodC (oppositeC C) D)
+                     (prodC (oppositeC D) D)
+                     (@set_cat) (@hom_functor D)
+                     (@pairF (oppositeC C)
+                             (oppositeC D) D D
+                             (@oppositeF C D F) (identityF D)))
+                  (@composeF
+                     (prodC (oppositeC C) D)
+                     (prodC (oppositeC C) C)
+                     (@set_cat) (@hom_functor C)
+                     (@pairF (oppositeC C)
+                             (oppositeC C) D C
+                             (identityF (oppositeC C)) G))
+    }.
+End Adjunction.
\ No newline at end of file
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f92ea027d..097865648 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1251,6 +1251,11 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
+let collect_evars_of_term evd c ty =
+  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+  evars (Evd.from_ctx (Evd.evar_universe_context evd))
+
 let do_program_recursive local p fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info = 
@@ -1268,8 +1273,9 @@ let do_program_recursive local p fixkind fixl ntns =
     and typ =
       nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
     in
+    let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
-      Obligations.eterm_obligations env id evd
+      Obligations.eterm_obligations env id evm
 	(List.length rec_sign) def typ
     in (id, def, typ, imps, evars)
   in