diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-17 07:12:05 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-17 07:12:05 +0000 |
| commit | 9e7bddc09f965e3a9caa23ca4723f893017351cb (patch) | |
| tree | 9a91b8988b4236ec2871c778a855e5ca75bc9e66 /tactics | |
| 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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
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 |