Mécanisme plus simple et efficace pour traduire les implicites

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

4 files changed, 23 insertions, 2 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a094e17ab8..472b636a8f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,6 +67,13 @@ let with_universes f = Options.with_option print_universes f
 let without_symbols f = Options.with_option print_no_symbol f
 let with_meta_as_hole f = Options.with_option print_meta_as_hole f
 
+(* For the translator *)
+let temporary_implicits_out = ref []
+let set_temporary_implicits_out l = temporary_implicits_out := l
+let get_temporary_implicits_out id =
+  try List.assoc id !temporary_implicits_out
+  with Not_found -> []
+
 (**********************************************************************)
 (* Various externalisation functions *)
 
@@ -230,7 +237,7 @@ let rec extern inctx scopes vars r =
 	       args
 	 | RVar (loc,id) -> (* useful for translation of inductive *)
 	     let args = List.map (extern true scopes vars) args in
-	     extern_app loc (implicits_of_global_out (VarRef id))
+	     extern_app loc (get_temporary_implicits_out id)
 	       (Ident (loc,id))
 	       args
 	 | _       -> 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b2dd833aaf..cb58ca58ee 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -61,3 +61,7 @@ val without_symbols : ('a -> 'b) -> 'a -> 'b
 
 (* This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(* For v8 translation *)
+val set_temporary_implicits_out :
+  (identifier * Impargs.implicits_list) list -> unit
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 641ccf7fc5..ffed01a34e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,10 @@ let for_grammar f x =
   interning_grammar := false;
   a
 
+(* For the translator *)
+let temporary_implicits_in = ref []
+let set_temporary_implicits_in l = temporary_implicits_in := l
+
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -183,7 +187,9 @@ let intern_reference env lvar = function
 	(* Extra allowance for grammars *)
 	if !interning_grammar then begin
 	  set_var_scope loc id env lvar;
-	  RVar (loc,id), [], []
+	  RVar (loc,id), 
+	  (try List.assoc id !temporary_implicits_in with Not_found -> []),
+	  []
 	end
 	else raise e
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 99e7d68bbc..b135caf505 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -93,3 +93,7 @@ val interp_aconstr : identifier list -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
+
+(* For v8 translation *)
+val set_temporary_implicits_in :
+  (identifier * Impargs.implicits_list) list -> unit