Extraction with implicits: perform the occur-check after optimisations

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

1 files changed, 12 insertions, 0 deletions

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 7e8127fb3e..4ed6e9a084 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -346,12 +346,24 @@ let rec depcheck_struct = function
       let lse' = depcheck_se lse in
       (mp,lse')::struc'
 
+let check_implicits = function
+  | MLexn s ->
+      if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then
+	begin
+	  if String.sub s 0 7 = "UNBOUND" then assert false;
+	  if String.sub s 0 8 = "IMPLICIT" then
+	    error_non_implicit (String.sub s 9 (String.length s - 9));
+	end;
+      false
+  | _ -> false
+
 let optimize_struct to_appear struc =
   let subst = ref (Refmap.empty : ml_ast Refmap.t) in
   let opt_struc =
     List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
   in
   let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
+  ignore (struct_ast_search check_implicits opt_struc);
   try
     if modular () then raise NoDepCheck;
     reset_needed ();