Fixed a Not_found bug when declaring in a section some implicit

arguments for a constant not defined in the section.

Also fixed some typos in the doc of implicit arguments in the
reference manual.

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

3 files changed, 15 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 472d7903b8..2da5bec186 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1208,15 +1208,15 @@ have to) be skipped in any expression involving an application of
 \item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any, enforcing the implicit arguments known
 from inside the section to be the ones declared by the command.
 
 \item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
-{\qualid} declared by this commands to contexts that requires the
+When in a module, tell not to activate the implicit arguments of
+{\qualid} declared by this command to contexts that require the
 module.
 
 \item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}}
@@ -1283,13 +1283,13 @@ and also~\ref{SetMaximalImplicitInsertion}).
 \item {\tt Global Arguments {\qualid} : default implicits
 \comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
 \item {\tt Local Arguments {\qualid} : default implicits
 \comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
+When in a module, tell not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the
 module.
 
diff --git a/library/impargs.ml b/library/impargs.ml
index badb69cb1e..ef7f592164 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -506,18 +506,23 @@ let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
+    (try
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
       let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
+    with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
+    (try
       let con' = pop_con con in
       let vars = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
       let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
 	Some (ImplConstant (con',flags),l')
+    with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
+    (try
       let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
@@ -525,6 +530,7 @@ let discharge_implicits (_,(req,l)) =
 	 List.map (add_section_impls vars extra_impls) l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
+    with Not_found -> (* ref not defined in this section *) Some (req,l))
 
 let rebuild_implicits (req,l) =
   match req with
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index b286538316..e8019a908f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -120,3 +120,7 @@ Check C2 eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
+
+(* Check global implicit declaration over ref not in section *)
+
+Section D. Global Arguments eq [A] _ _. End D.