Fix bugs related to Program integration.

- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.

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

15 files changed, 86 insertions, 34 deletions

diff --git a/CHANGES b/CHANGES
index b587e2ecc..4a5c74410 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,8 @@ Changes from V8.4
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
+- "Solve Obligations using" changed to "Solve Obligations with",
+  consistent with "Proof with".
 
 Changes from V8.4beta to V8.4
 =============================
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0f7705317..871f161ab 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -337,6 +337,8 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_glob_constr tomatch) in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
+  let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
+  evdref := evd;
   let typ = nf_evar !evdref j.uj_type in
   let t =
     try try_find_ind env !evdref typ realnames
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2b93a5fca..327745616 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -219,8 +219,11 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 			   let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
 			     isevars := evs;
 			     let (n, dom, rng) = destLambda t in
-			     let (domk, args) = destEvar dom in
-			       isevars := define domk a !isevars;
+			     let dom = whd_evar !isevars dom in
+			       if isEvar dom then
+				 let (domk, args) = destEvar dom in
+				   isevars := define domk a !isevars;
+			       else ();
 			       t, rng
 		       | _ -> raise NoSubtacCoercion
 		     in
@@ -228,8 +231,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		     let env' = push_rel (make_name "x", None, a) env in
 		     let c2 = coerce_unify env' b b' in
 		       match c1, c2 with
-		       None, None ->
-			 None
+		       | None, None -> None
 		       | _, _ ->
 			   Some
 			     (fun x ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8fe06539c..be335ac91 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -480,9 +480,10 @@ let mark_resolvability_undef b evi =
 
 let mark_resolvability b evi =
   assert (evi.evar_body = Evar_empty);
-  mark_resolvability_undef false evi
+  mark_resolvability_undef b evi
 
 let mark_unresolvable evi = mark_resolvability false evi
+let mark_resolvable evi = mark_resolvability true evi
 
 let mark_resolvability b sigma =
   Evd.fold_undefined (fun ev evi evs ->
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3d36168fd..67336b340 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -85,6 +85,7 @@ val instance_constructor : typeclass -> constr list -> constr option * types
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
+val mark_resolvable : evar_info -> evar_info
 val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4a850db66..125ef94dc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -635,6 +635,23 @@ let has_undefined p oevd evd =
     snd (p oevd ev evi))
     evd false
 
+(** Revert the resolvability status of evars after resolution,
+    potentially unprotecting some evars that were set unresolvable
+    just for this call to resolution. *)
+
+let revert_resolvability oevd evd = 
+  Evd.fold_undefined
+    (fun ev evi evm ->
+     try 
+       if not (Typeclasses.is_resolvable evi) then
+	 let evi' = Evd.find_undefined oevd ev in
+	   if Typeclasses.is_resolvable evi' then
+	     Evd.add evm ev (Typeclasses.mark_resolvable evi)
+	   else evm
+       else evm
+     with Not_found -> evm)
+  evd evd
+
 (** If [do_split] is [true], we try to separate the problem in
     several components and then solve them separately *)
 
@@ -645,7 +662,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
   let in_comp comp ev = if do_split then Intset.mem ev comp else true
   in
   let rec docomp evd = function
-    | [] -> evd
+    | [] -> revert_resolvability oevd evd
     | comp :: comps ->
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
index a6ce4de0f..5f17f7af3 100644
--- a/test-suite/bugs/closed/shouldsucceed/2083.v
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -15,7 +15,7 @@ Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
 
 Require Import Omega.
 
-Solve Obligations using program_simpl ; auto with *; try omega.
+Solve Obligations with program_simpl ; auto with *; try omega.
 
 Next Obligation.
   apply H. simpl. omega.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 00a13aed0..f8d3ad2c3 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -100,6 +100,6 @@ Next Obligation. simpl in *; intros.
   apply H. simpl. omega.
 Qed.
 
-Program Fixpoint check_n'  (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
+Program Fixpoint check_n'  (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})
   {measure (p - n) p} : nat :=
-  _.
+  _.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index e0d7a3d7a..8e491b1b8 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -224,7 +224,7 @@ Hint Extern 4 (subrelation (inverse _) _) =>
   class_apply @subrelation_symmetric : typeclass_instances.
 
 (** The complement of a relation conserves its proper elements. *)
-Set Printing All.
+
 Program Definition complement_proper
   `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
   Proper (RA ==> RA ==> iff) (complement R) := _.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ceaab3d0f..9d259eee1 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -280,7 +280,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		  match term with 
 		  | Some t -> 
 		      let obls, _, constr, typ = 
-			Obligations.eterm_obligations env id !evars evm 0 t termtype
+			Obligations.eterm_obligations env id !evars 0 t termtype
 		      in obls, Some constr, typ
 		  | None -> [||], None, termtype
 		in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b4e9daa1..3657c5d5a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -141,9 +141,9 @@ let do_definition ident k bl red_option c ctypopt hook =
 	| Some t -> t
 	| None -> Retyping.get_type_of env evd c
       in 
-      let evm = Obligations.non_instanciated_map env (ref evd) evd in
+      Obligations.check_evars env evd;
       let obls, _, c, cty = 
-	Obligations.eterm_obligations env ident evd evm 0 c typ
+	Obligations.eterm_obligations env ident evd 0 c typ
       in
 	ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
@@ -282,6 +282,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
 
   (* Instantiate evars and check all are resolved *)
   let evd = consider_remaining_unif_problems env_params !evdref in
+  let evd = Typeclasses.mark_resolvables evd in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
   let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
@@ -714,9 +715,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   in
   let fullcoqc = Evarutil.nf_evar !isevars def in
   let fullctyp = Evarutil.nf_evar !isevars typ in
-  let evm = Obligations.non_instanciated_map env isevars !isevars in
+  Obligations.check_evars env !isevars;
   let evars, _, evars_def, evars_typ = 
-    Obligations.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp 
+    Obligations.eterm_obligations env recname !isevars 0 fullcoqc fullctyp 
   in
     ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook)
 
@@ -885,7 +886,7 @@ let do_program_recursive fixkind fixl ntns =
       Termops.it_mkNamedProd_or_LetIn typ rec_sign
     in
     let evars, _, def, typ = 
-      Obligations.eterm_obligations env id evd (Evd.undefined_evars evd)
+      Obligations.eterm_obligations env id evd 
 	(List.length rec_sign) 
 	(nf_evar evd def) (nf_evar evd typ)
     in (id, def, typ, imps, evars)
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 9840814b1..7f5991d38 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -46,6 +46,8 @@ open Pcoq
 open Prim
 open Constr
 
+let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+
 GEXTEND Gram
   GLOBAL: withtac;
 
@@ -53,6 +55,12 @@ GEXTEND Gram
     [ [ "with"; t = Tactic.tactic -> Some t
       | -> None ] ]
   ;
+
+  Constr.closed_binder:
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
+	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+          [LocalRawAssum ([id], default_binder_kind, typ)]
+    ] ];
   
   END
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 529228d01..589403882 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -44,17 +44,17 @@ let succfix (depth, fixrels) =
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
-let non_instanciated_map env evd evm =
-  List.fold_left
-    (fun evm (key, evi) ->
-       let (loc,k) = evar_source key !evd in
-	 match k with
-	 | QuestionMark _ -> Evd.add evm key evi
-	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
-	 | _ ->
-	     Pretype_errors.error_unsolvable_implicit loc env
-	       evm (Evarutil.nf_evar_info evm evi) k None)
-    Evd.empty (Evarutil.non_instantiated evm)
+let check_evars env evm =
+  List.iter
+  (fun (key, evi) ->
+   let (loc,k) = evar_source key evm in
+     match k with
+     | QuestionMark _
+     | ImplicitArg (_,_,false) -> ()
+     | _ ->
+       Pretype_errors.error_unsolvable_implicit loc env
+         evm (Evarutil.nf_evar_info evm evi) k None)
+  (Evd.undefined_list evm)
 
 type oblinfo =
   { ev_name: int * identifier;
@@ -223,11 +223,12 @@ let map_evar_info f evi =
     evar_concl = f evi.evar_concl;
     evar_body = map_evar_body f evi.evar_body }
     
-let eterm_obligations env name isevars evm fs ?status t ty = 
+let eterm_obligations env name evm fs ?status t ty = 
   (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
   let nc_len = Sign.named_context_length nc in
-  let evl = List.rev (to_list evm) in
+  let evm = Evarutil.nf_evar_map_undefined evm in
+  let evl = List.rev (Evarutil.non_instantiated evm) in
   let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
   let sevl = sort_dependencies evl in
   let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
@@ -250,7 +251,7 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	   | Some t -> t, trunc_named_context fs hyps, fs
 	   | None -> evtyp, hyps, 0
 	 in
-	 let loc, k = evar_source id isevars in
+	 let loc, k = evar_source id evm in
 	 let status = match k with QuestionMark o -> Some o | _ -> status in
 	 let status, chop = match status with
 	   | Some (Define true as stat) ->
@@ -984,3 +985,18 @@ let next_obligation n tac =
     try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
     with Not_found -> anomaly "Could not find a solvable obligation."
   in solve_obligation prg i tac
+
+
+let init_program () =
+  Coqlib.check_required_library ["Coq";"Init";"Datatypes"];
+  Coqlib.check_required_library ["Coq";"Init";"Specif"];
+  Coqlib.check_required_library ["Coq";"Program";"Tactics"]
+
+
+let set_program_mode c =
+  if c then
+    if !Flags.program_mode then ()
+    else begin
+      init_program ();
+      Flags.program_mode := true;
+    end
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 1758082e8..16c00ce8f 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -29,7 +29,7 @@ val declare_definition_ref :
      Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference declaration_hook -> global_reference) ref
 
-val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map
+val check_evars : env -> evar_map -> unit
 
 val mkMetas : int -> constr list
 
@@ -38,7 +38,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
 
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
+val eterm_obligations : env -> identifier -> evar_map -> int ->
   ?status:obligation_definition_status -> constr -> types -> 
   (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
       tactic option) array
@@ -115,3 +115,5 @@ val admit_obligations : Names.identifier option -> unit
 exception NoObligations of Names.identifier option
 
 val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds
+
+val set_program_mode : bool -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 20c9531fe..c727cc918 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1579,8 +1579,8 @@ let interp c = match c with
 
 let interp c = 
   let mode = Flags.is_program_mode () in
-  let flag = mode || !program_flag in
-    Flags.program_mode := flag;
+    (try Obligations.set_program_mode !program_flag
+     with e -> program_flag := false; raise e);
     interp c; check_locality ();
     program_flag := false;
     Flags.program_mode := mode