From 0931ccb78d2555e5c38da66a2e2cd7afc6ae7e94 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 17 Sep 2010 14:12:53 +0000
Subject: Extraction: multiple fixes related with the Not_found encountered by
 X. Leroy

Cf. coqdev for the details of the bug report.

 - Protect some Hashtbl.find and other risky functions in order to avoid
   as much as possible to end with an irritating Anomaly : Not_found.
 - Re-enable in pp_ocaml_extern the case of a module-file used as
   a module (e.g. module A' := A for A.v) when doing modular extraction.
 - Rework the code that decides to "open" or not modules initially:
   opening A when A contains a submodule B hides the file B even when
   B isn't opened itself, we avoid that now.
 - Fix some tables (sets or maps) used by extraction for which it is
   critical to consider constants/inductives/global_reference _not_
   modulo the equivalence of Elie, but rather via Pervasives.compare.

 Still to do : avoid appearance of '_a in extracted code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13424 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/mlutil.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction/mlutil.mli')

diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index b55766ed32..022e42fddc 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -11,6 +11,7 @@ open Names
 open Term
 open Libnames
 open Miniml
+open Table
 
 (*s Utility functions over ML types with meta. *)
 
@@ -106,7 +107,7 @@ val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 val ast_subst : ml_ast -> ml_ast -> ml_ast
 
-val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast
 
 val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
-- 
cgit v1.2.3