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 --- tactics/class_tactics.ml4 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tactics/class_tactics.ml4') 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 -- cgit v1.2.3