Declaration of multiple hypotheses or parameters now share typing

information for inference of implicit arguments.

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

5 files changed, 42 insertions, 25 deletions

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index a654080de8..f702aa62f1 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -17,3 +17,7 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
     | vnil => w
     | vcons a v' => vcons a (app v' w)
   end.
+
+(* Test sharing information between different hypotheses *)
+
+Parameters (a:_) (b:a=0).
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 78848f1c2a..7278cc4c1b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -346,8 +346,8 @@ let context l =
       let impl = List.exists test impls in
       let decl = (Discharge, Definitional) in
       let nstatus =
-        Command.declare_assumption false decl t [] impl
-          Vernacexpr.NoInline (Loc.ghost, id)
+        snd (Command.declare_assumption false decl t [] impl
+          Vernacexpr.NoInline (Loc.ghost, id))
       in
       status && nstatus
   in List.fold_left fn true (List.rev ctx)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6c69495c5f..1071605fcd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -188,7 +188,7 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca
   let r = VarRef ident in
   let () = Typeclasses.declare_instance None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true in
-  true
+  (r,true)
 | Global | Local | Discharge ->
   let local = get_locality ident local in
   let inl = match nl with
@@ -204,19 +204,38 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca
   let () = Autoinstance.search_declaration (ConstRef kn) in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr local in
-  Lib.is_modtype_strict ()
+  (gr,Lib.is_modtype_strict ())
 
 let declare_assumptions_hook = ref ignore
 let set_declare_assumptions_hook = (:=) declare_assumptions_hook
 
-let interp_assumption bl c =
+let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
-  let env = Global.env () in
-  interp_type_evars_impls env c
+  interp_type_evars_impls ~evdref ~fail_evar:false env c
 
 let declare_assumptions idl is_coe k c imps impl_is_on nl =
   !declare_assumptions_hook c;
-  List.fold_left (fun status id -> declare_assumption is_coe k c imps impl_is_on nl id && status) true idl
+  List.fold_left (fun (refs,status) id ->
+    let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in
+    ref'::refs, status' && status) ([],true) idl
+
+let do_assumptions kind nl l =
+  let env = Global.env () in
+  let evdref = ref Evd.empty in
+  let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
+    let t,imps = interp_assumption evdref env [] c in
+    let env =
+      push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
+    (env,((is_coe,idl),t,imps))) env l in
+  let evd = consider_remaining_unif_problems env !evdref in
+  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
+  let l = List.map (on_pi2 (nf_evar evd)) l in
+  List.iter (fun (_,c,_) -> check_evars env Evd.empty evd c) l;
+  snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,imps) ->
+    let t = replace_vars subst t in
+    let (refs,status') = declare_assumptions idl is_coe kind t imps false nl in
+    let subst' = List.map2 (fun (_,id) c -> (id,constr_of_global c)) idl refs in
+    (subst'@subst, status' && status)) ([],true) l)
 
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7e7586c5cc..6d4f6c09c4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -44,18 +44,15 @@ val do_definition : Id.t -> definition_kind ->
 
 (** {6 Parameters/Assumptions} *)
 
-val interp_assumption :
-  local_binder list -> constr_expr -> types * Impargs.manual_implicits
-
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   Impargs.manual_implicits ->
-  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> bool
+  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+  global_reference * bool
 
-val declare_assumptions : variable Loc.located list ->
-  coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits ->
-  bool -> Vernacexpr.inline -> bool
+val do_assumptions : locality * assumption_object_kind ->
+  Vernacexpr.inline -> simple_binder with_coercion list -> bool
 
 (** {6 Inductive and coinductive types} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8cf3767cb2..3395bea150 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -529,19 +529,16 @@ let vernac_exact_proof c =
   save_named true;
   Backtrack.mark_unreachable [prf]
 
-let vernac_assumption locality (local, kind) l nl=
+let vernac_assumption locality (local, kind) l nl =
   let local = enforce_locality_exp locality local in
   let global = local == Global in
   let kind = local, kind in
-  let status =
-    List.fold_left (fun status (is_coe,(idl,c)) ->
-      if Dumpglob.dump () then
-	List.iter (fun lid ->
-	  if global then Dumpglob.dump_definition lid false "ax"
-	  else Dumpglob.dump_definition lid true "var") idl;
-      let t,imps = interp_assumption [] c in
-      declare_assumptions idl is_coe kind t imps false nl && status) true l
-  in
+  List.iter (fun (is_coe,(idl,c)) ->
+    if Dumpglob.dump () then
+      List.iter (fun lid ->
+	if global then Dumpglob.dump_definition lid false "ax"
+	else Dumpglob.dump_definition lid true "var") idl) l;
+  let status = do_assumptions kind nl l in
   if not status then Pp.feedback Interface.AddedAxiom
 
 let vernac_record k finite infer struc binders sort nameopt cfs =