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

6 files changed, 51 insertions, 24 deletions

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