diff options
author | 2008-05-17 07:12:05 +0000 | |
---|---|---|
committer | 2008-05-17 07:12:05 +0000 | |
commit | 9e7bddc09f965e3a9caa23ca4723f893017351cb (patch) | |
tree | 9a91b8988b4236ec2871c778a855e5ca75bc9e66 | |
parent | 6c4cb0b91468ac0f7bc95d79f89b88417628127a (diff) |
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
-rw-r--r-- | Makefile.build | 2 | ||||
-rwxr-xr-x | configure | 4 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 3 | ||||
-rw-r--r-- | theories/Numbers/NumPrelude.v | 11 |
4 files changed, 7 insertions, 13 deletions
diff --git a/Makefile.build b/Makefile.build index 5e89e08fa..b0aeb16cf 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 @@ -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 6aadb9bbf..00f8179ca 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 f2f6b9082..05e905170 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. |