diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | config/Makefile.template | 3 | ||||
| -rwxr-xr-x | configure | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 7 |
4 files changed, 16 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index b0aeb16cf..4b4ba73e9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -73,7 +73,7 @@ OCAMLC += $(CAMLFLAGS) OCAMLOPT += $(CAMLFLAGS) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) -OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(CAMLTIMEPROF) $(USERFLAGS) +OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= -slash $(LOCALINCLUDES) CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements diff --git a/config/Makefile.template b/config/Makefile.template index f35af2b58..e5061ebe8 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -72,8 +72,9 @@ CAMLMKTOP="CAMLMKTOPEXEC" # Caml flags CAMLFLAGS=-rectypes CAMLANNOTATEFLAG -# Compilation debug flag +# Compilation debug flags CAMLDEBUG=COQDEBUGFLAG +CAMLDEBUGOPT=COQDEBUGFLAGOPT # User compilation flag USERFLAGS= @@ -87,6 +87,7 @@ camlp4oexec=camlp4o coq_debug_flag= +coq_debug_flag_opt= coq_profile_flag= coq_annotate_flag= best_compiler=opt @@ -412,6 +413,11 @@ case $CAMLVERSION in cflags="$cflags -DOCAML_307";; esac +if [ "$CAMLTAG" = "OCAML310" ] && [ "$coq_debug_flag" = "-g" ]; then + # Compilation debug flag + coq_debug_flag_opt="-g" +fi + # Camlp4 / Camlp5 configuration if [ "$camlp5dir" != "" ]; then @@ -882,6 +888,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|CAMLP4TOOL|$camlp4oexec|" \ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \ + -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \ diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 00f8179ca..618d48482 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -359,7 +359,12 @@ let full_eauto debug n lems gls = let typeclasses_eauto debug n lems gls = let dbnames = [typeclasses_db] in - let db_list = List.map searchtable_map dbnames in + let db_list = List.map + (fun x -> + try searchtable_map x + with Not_found -> (empty_transparent_state, Hint_db.empty)) + dbnames + in e_search_auto debug n lems db_list gls exception Found of evar_map |