- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)

- Makefile: typo apparente avec .ml4.preprocessed
- test-suite: ajout d'un test sur eta qui trainait dans le coin



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

3 files changed, 72 insertions, 35 deletions

diff --git a/Makefile.common b/Makefile.common
index a8edbee72..1be1d0dfb 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -865,7 +865,7 @@ STAGE1_TARGETS:= $(STAGE1) \
   $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
   $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \
   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml4.preprocessed)
+  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
 STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index fcce68b91..8c9712e97 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -201,3 +201,16 @@ Axiom silly_axiom : forall v : exp, v = v -> False.
 Lemma silly_lemma : forall x : atom, False.
 intros x.
 apply silly_axiom with (v := x).  (* fails *)
+reflexivity.
+Qed.
+
+(* Check that unification does not commit too early to a representative
+   of an eta-equivalence class that would be incompatible with other
+   unification constraints *)
+
+Lemma eta : forall f : (forall P, P 1),
+  (forall P, f P = f P) ->
+   forall Q, f (fun x => Q x) = f (fun x => Q x).
+intros.
+apply H. 
+Qed.
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 73c79b86c..abb348f3a 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -38,6 +38,11 @@ let rec print_list sep = function
   | x :: l -> print x; print sep; print_list sep l
   | [] -> ()
 
+let best_ocamlc = 
+  if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc"
+let best_ocamlopt =
+  if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt"
+
 let section s =
   let l = String.length s in
   let sep = String.make (l+5) '#'
@@ -156,27 +161,7 @@ let variables l =
     | _ :: r -> var_aux r
   in
     section "Variables definitions.";
-    print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; 
-    if Coq_config.local then
-      (print "COQSRC:=$(COQTOP)\n";
-       print "COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-  -I $(COQTOP)/library -I $(COQTOP)/parsing \\
-  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
-  -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
-  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\
-  -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\
-  -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\
-  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\
-  -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\
-  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
-  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
-  -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
-  -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
-  -I $(CAMLP4LIB)\n")
-    else
-      (print "COQSRC:=$(shell $(COQBIN)coqc -where)\n"; 
-       print "COQSRCLIBS:=-I $(COQSRC)\n");
-    print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n";
+    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n";
     if !opt = "-byte" then 
       print "override OPT:=-byte\n"
     else
@@ -189,17 +174,14 @@ let variables l =
     print "GALLINA:=$(COQBIN)gallina\n";
     print "COQDOC:=$(COQBIN)coqdoc\n";
     (* Caml executables and relative variables *)
-    printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
-    printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n";
-    printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n";
-    printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n";
+    printf "CAMLC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlopt;
+    printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
+    printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
     print "GRAMMARS:=grammar.cma\n";
     print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
-
-    (if Coq_config.local then
-      print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"
-    else
-      print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"); 
+    print "CAMLP4OPTIONS=\n";
+    print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
     var_aux l;
     print "\n"
 
@@ -226,6 +208,15 @@ let dir_of_target t =
     | Include dir -> dir
     | _ -> assert false
 
+let parameters () =
+  print "# \n";
+  print "# Compilation looks in the path for coqtop; set COQBIN if coqtop is not in path\n";
+  print "# if .ml files have to be compiled, set CAMLBIN if ocamlc is not in path\n";
+  print "# if .ml files have to be compiled, set CAMLP4BIN if camlp4/5 is not in path\n";
+  print "# \n";
+  print "# set COQTOP to a Coq source directory for compiling over Coq compiled sources\n";
+  print "# \n\n"
+
 let include_dirs l =
   let rec split_includes l = 
     match l with
@@ -253,12 +244,44 @@ let include_dirs l =
   let str_i = parse_includes inc_i in
   let str_i' = parse_includes inc_i' in
   let str_r = parse_includes inc_r in
-    section "Libraries definition.";
-    print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+    section "Libraries definitions.";
+    printf "CAMLP4:=%s\n" Coq_config.camlp4;
+    print "ifdef CAMLP4BIN\n";
+    print "  CAMLP4LIB:=$(shell $(CAMLP4BIN)/$(CAMLP4) -where 2> /dev/null)\n";
+    print "else\n";
+    print "  CAMLP4LIB:=$(shell $(CAMLP4) -where 2> /dev/null)\n";
+    print "endif\n";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
+    print "COQLIB:=$(shell $(COQBIN)coqtop -where 2> /dev/null)\n";
+    print "ifdef COQTOP # set COQTOP for compiling from Coq sources\n";
+    print "  COQBIN:=$(COQTOP)/bin\n";
+    print "  COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+  -I $(COQTOP)/library -I $(COQTOP)/parsing \\
+  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
+  -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
+  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc -I $(COQTOP)/contrib/dp \\
+  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
+  -I $(COQTOP)/contrib/firstorder -I $(COQTOP)/contrib/fourier \\
+  -I $(COQTOP)/contrib/funind -I $(COQTOP)/contrib/interface \\
+  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
+  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
+  -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
+  -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml\n";
+    print "else ifneq ($(strip $(COQLIB)),)\n";
+    print "  COQSRCLIBS:=-I $(COQLIB)\n";
+    print "else\n";
+    print "  $(error Cannot find coqtop in path; set variable COQBIN to the directory where coqtop is located)\n";
+    print "endif\n";
+    if List.exists (function ML _ -> true | _ -> false) l then
+      begin
+	print "ifeq ($(strip $(CAMLP4LIB)),)\n";
+	print "  $(error Cannot find $(CAMLP4) in path; set variable CAMLP4BIN to the directory where $(CAMLP4) is located)\n";
+	print "endif\n";
+      end;
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
+
 let rec special = function
   | [] -> []
   | Special (file,deps,com) :: r -> (file,deps,com) :: (special r)
@@ -423,10 +446,10 @@ let banner () =
 ##  v      #                  The Coq Proof Assistant                   ##
 ## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
 ##   \\VV/  #                                                            ##
-##    //   #   Makefile automagically generated by coq_makefile V%s    ##
+##    //   #  Makefile automagically generated by coq_makefile V%s ##
 ##########################################################################
 
-" Coq_config.version)
+" (Coq_config.version ^ String.make (7 - String.length Coq_config.version) ' '))
 
 let warning () =
   print "# WARNING\n#\n";
@@ -467,6 +490,7 @@ let do_makefile args =
     banner ();
     warning ();
     command_line args;
+    parameters ();
     include_dirs l;
     variables l;
     all_target l;