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/table.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7b6010229..a0cffa596 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -11,6 +11,9 @@ open Libnames open Miniml open Declarations +module Refset' : Set.S with type elt = global_reference +module Refmap' : Map.S with type key = global_reference + val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) -- cgit v1.2.3