From c182c9e8beb5c950b7c565fd1db58f63c7fa213b Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 8 Aug 2012 15:13:04 +0000
Subject: Fixup for macOS 10.8 & Ocaml 4.0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build                                | 2 +-
 Makefile.common                               | 4 ++--
 plugins/funind/functional_principles_types.ml | 6 ------
 3 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 7fa1d992d2..e6cba45efb 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -98,7 +98,7 @@ $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
 $(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
-CAMLP4DEPS=$(shell sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
+CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 else
diff --git a/Makefile.common b/Makefile.common
index 1ede038364..c10a02e265 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -71,8 +71,8 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 SRCDIRS:=\
   config 	tools 		tools/coqdoc 	scripts		lib \
   kernel	kernel/byterun	library 	proofs 		tactics \
-  pretyping	interp		toplevel/utils	toplevel 	parsing \
-  printing	grammar 	intf            ide/utils	ide	\
+  pretyping	interp		toplevel 	parsing		printing \
+  grammar 	intf            ide/utils	ide	\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote \
     setoid_ring xml 		extraction 	fourier \
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 42e5c36a8c..567bdcd6ef 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -144,12 +144,6 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 (*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
     res
   in
-  let rec has_dummy_var t  =
-    fold_constr
-      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
-      false
-      t
-  in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
       match kind_of_term pre_princ with
-- 
cgit v1.2.3