From 9e7bddc09f965e3a9caa23ca4723f893017351cb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 17 May 2008 07:12:05 +0000
Subject: Fix a de Bruijn bug in setoid_rewrite when rewriting under a
 non-dependent product under a lambda. Now qiff can be replaced by a simple
 setoid_rewrite in NumPrelude. Change configure to not do stripping if
 compiling with -g... Add -g / CAMLDEBUG flags to the native compilation
 command too.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10941 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build                |  2 +-
 configure                     |  4 ++--
 tactics/class_tactics.ml4     |  3 ++-
 theories/Numbers/NumPrelude.v | 11 ++---------
 4 files changed, 7 insertions(+), 13 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 5e89e08fa9..b0aeb16cff 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -73,7 +73,7 @@ OCAMLC += $(CAMLFLAGS)
 OCAMLOPT += $(CAMLFLAGS)
 
 BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS)
+OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS= -slash $(LOCALINCLUDES)
 
 CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements 
diff --git a/configure b/configure
index 1771756c85..07bea069a7 100755
--- a/configure
+++ b/configure
@@ -271,7 +271,7 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
@@ -579,7 +579,7 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6aadb9bbfc..00f8179cab 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -724,7 +724,7 @@ let unify_eqn env sigma hypinfo t =
 let unfold_impl t =
   match kind_of_term t with
     | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) -> 
-	mkProd (Anonymous, a, b)
+	mkProd (Anonymous, a, lift 1 b)
     | _ -> assert false
 
 let unfold_id t = 
@@ -820,6 +820,7 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
 		    
 	    | Prod (_, x, b) when not (dependent (mkRel 1) b) -> 
 		let x', occ = aux env x occ None in
+		let b = subst1 mkProp b in
 		let b', occ = aux env b occ None in
 		let res = 
 		  if x' = None && b' = None then None
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index f2f6b90822..05e9051708 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -164,7 +164,7 @@ unfold predicate_wd;
 let x := fresh "x" in
 let y := fresh "y" in
 let H := fresh "H" in
-  intros x y H; qiff x y H.
+  intros x y H; setoid_rewrite H; reflexivity.
 
 (* solve_relation_wd solves the goal [relation_wd R] for R consisting of
 morhisms and quatifiers *)
@@ -178,14 +178,7 @@ let x2 := fresh "x" in
 let y2 := fresh "y" in
 let H2 := fresh "H" in
   intros x1 y1 H1 x2 y2 H2;
-  rewrite H1;
-  qiff x2 y2 H2.
-
-(* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite
-uses qiff to take the formula apart in order to make it quantifier-free,
-and then qiff is called again and takes the formula apart for the second
-time. It is better to analyze the formula once and generalize qiff to take
-a list of equalities that it has to rewrite. *)
+  rewrite H1; setoid_rewrite H2; reflexivity.
 
 (* The following tactic uses solve_predicate_wd to solve the goals
 relating to well-defidedness that are produced by applying induction.
-- 
cgit v1.2.3