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

1 files changed, 6 insertions, 0 deletions

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