Protection contre des arguments farfelus pour les implicites manuels

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

1 files changed, 30 insertions, 1 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 4d12d9ac18..d71acd70fc 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -262,7 +262,36 @@ let declare_implicits = function
       let imps = (snd mib_imps.(i)).(j-1) in
       add_anonymous_leaf (in_constructor_implicits (consp, imps))
 
-let declare_manual_implicits r l = match r with
+let context_of_global_reference = function
+  | VarRef sp -> []
+  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
+  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
+  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
+
+let type_of_global r =
+  let args = 
+    Array.of_list
+      (Sign.instance_from_section_context (context_of_global_reference r)) in
+  match r with
+  | VarRef sp ->
+      lookup_named_type (basename sp) (Global.env ())
+  | ConstRef sp ->
+      Typeops.type_of_constant (Global.env ()) Evd.empty (sp,args)
+  | IndRef sp -> 
+      Typeops.type_of_inductive (Global.env ()) Evd.empty (sp,args)
+  | ConstructRef sp ->
+      Typeops.type_of_constructor (Global.env ()) Evd.empty (sp,args)
+
+let check_range n i =
+  if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+
+let declare_manual_implicits r l =
+  let t = type_of_global r in
+  let n = List.length (fst (splay_prod (Global.env()) Evd.empty t)) in
+  if not (list_distinct l) then error ("Some numbers occur several time");
+  List.iter (check_range n) l;
+  let l = List.sort (-) l in
+  match r with
   | VarRef sp -> 
       add_anonymous_leaf (in_var_implicits (sp,Impl_manual l))
   | ConstRef sp ->