Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk

(résolution entre autres des bugs 1882, 1883, 1884).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 96 insertions, 29 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index e7423c748..074dd0901 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -406,7 +406,6 @@ let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
   let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
-  let c_typ = clenv_hnf_constr clenv' c_typ in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5edd6054..58e9aca9e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -492,10 +492,12 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       else
 	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
 
-let choose_less_dependent_instance evk evd =
+let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
-  let ctx = evar_filtered_context evi in
-  Evd.evar_define evk (mkVar (pi1 (List.hd ctx))) evd
+  let subst = make_pure_subst evi args in
+  let subst' = List.filter (fun (id,c) -> c = term) subst in
+  if subst' = [] then error "Too complex unification problem" else
+  Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
   let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in
@@ -506,13 +508,13 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
   | Evar (evk1,args1), Rel _ when l1 = [] & l2 = [] ->
       (* The typical kind of constraint coming from patter-matching return
          type inference *)
-      assert (array_for_all ((=) term2) args1);
-      choose_less_dependent_instance evk1 evd, true
+      assert (array_for_all (fun a -> a = term2 or isEvar a) args1);
+      choose_less_dependent_instance evk1 evd term2 args1, true
   | Rel _, Evar (evk2,args2) when l1 = [] & l2 = [] ->
       (* The typical kind of constraint coming from patter-matching return
          type inference *)
       assert (array_for_all ((=) term1) args2);
-      choose_less_dependent_instance evk2 evd, true
+      choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       first_order_unification env evd (ev1,l1) appr2
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9a9d75eb8..27e964b6a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -48,6 +48,8 @@ val e_new_evar :
 val new_evar_instance :
  named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr
 
+val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
+
 (***********************************************************)
 (* Instantiate evars *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 41d6ff4c1..108e21f67 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -406,19 +406,26 @@ let pose_all_metas_as_evars env evd t =
   (* side-effect *)
   (!evdref, c)
 
+let try_to_coerce env evd c cty tycon =
+  let j = make_judge c cty in
+  let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+  let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
+  if b then
+    let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
+    (evd',j'.uj_val)
+  else
+    error "Cannot solve unification constraints"
+
 let w_coerce_to_type env evd c cty mvty =
-  try
-    let j = make_judge c cty in
-    let evd,mvty = pose_all_metas_as_evars env evd mvty in
-    let tycon = mk_tycon_type mvty in
-    let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
-    let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
-    if b then
-      let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
-      (evd',j'.uj_val)
-    else (evd,c)
+  let evd,mvty = pose_all_metas_as_evars env evd mvty in
+  let tycon = mk_tycon_type mvty in
+  try try_to_coerce env evd c cty tycon
   with e when precatchable_exception e ->
-    (evd,c)
+    (* inh_conv_coerce_rigid_to should have reasoned modulo reduction 
+       but there are cases where it though it was not rigid (like in
+       fst (nat,nat)) and stops while it could have seen that it is rigid *)
+    let cty = Tacred.hnf_constr env (evars_of evd) cty in
+    try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
   let cty = get_type_of env (evars_of evd) c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4ec8ee0ae..25e920976 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2385,12 +2385,7 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
 
 
 let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl =
-  (*test suivant sans doute inutile car refait par le letin_tac*)
-  if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
-    errorlabstrm "induction" 
-      (str "Cannot generalize a global variable");
   let indsign,scheme = elim_info in
-
   let indref = match scheme.indref with | None -> assert false | Some x -> x in
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
   let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index deeab4cb6..fcce68b91 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -185,3 +185,19 @@ intro.
 eapply H.
 apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
 Defined.
+
+(* Fine-tuning coercion insertion in presence of unfolding (bug #1883) *)
+
+Parameter name : Set.
+Definition atom := name.
+
+Inductive exp : Set :=
+  | var : atom -> exp.
+
+Coercion var : atom >-> exp.
+
+Axiom silly_axiom : forall v : exp, v = v -> False.
+
+Lemma silly_lemma : forall x : atom, False.
+intros x.
+apply silly_axiom with (v := x).  (* fails *)
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 02f88b727..5aa78816b 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -36,3 +36,22 @@ Theorem Refl : forall P, P <-> P. tauto. Qed.
 Goal True.
 case Refl || ecase Refl.
 Abort.
+
+
+(* Submitted by B. Baydemir (bug #1882) *)
+
+Require Import List.
+
+Definition alist R := list (nat * R)%type.
+
+Section Properties.
+  Variables A : Type.
+  Variables a : A.
+  Variables E : alist A.
+
+  Lemma silly : E = E.
+  Proof.
+    clear. induction E.  (* this fails. *)
+  Abort.
+
+End Properties.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index e117bf62f..082cbfbe1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -186,3 +186,27 @@ refine
 Abort.
 
 End Additions_while.
+
+(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
+
+Parameter F1 G1 : nat -> Prop.
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H)).
+Abort.
+
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+
+(* Remark: the following example does not succeed any longer in 8.2 because,
+   the algorithm is more general and does exclude a solution that it should
+   exclude for typing reason. Handling of types and backtracking is still to
+   be done
+
+Section S.
+Variables A B : nat -> Prop.
+Goal forall x : nat, A x -> B x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+End S.
+*)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 534b680e2..0baba94c6 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -765,7 +765,7 @@ let _ =
 
   pp "  Ltac zg_tac := try";
   pp "    (red; simpl Zcompare; auto;";
-  pp "     let t := fresh \"H\" in (intros t; discriminate H)).";
+  pp "     let t := fresh \"H\" in (intros t; discriminate t)).";
   pp "  Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
   pp "  Proof.";
   pp "  intros x; case x; clear x; unfold iter.";
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 67f017986..3138ce4ef 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -164,12 +164,15 @@ let variables l =
   -I $(COQTOP)/library -I $(COQTOP)/parsing \\
   -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
   -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
-  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\
-  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
-  -I $(COQTOP)/contrib/fourier \\
+  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\
+  -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\
+  -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\
+  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\
   -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\
-  -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\
-  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
+  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
+  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
+  -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
+  -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
   -I $(CAMLP4LIB)\n")
     else
       (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n";