From b687035e0156ee9723d940e6460c4049be54bf89 Mon Sep 17 00:00:00 2001 From: puech Date: Fri, 29 Jul 2011 14:30:06 +0000 Subject: Coq_micromega: generic = on constr replaced by eq_constr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14371 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/coq_micromega.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 50b01d751..1ad49bb8c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1107,17 +1107,17 @@ struct match kind_of_term term with | App(l,rst) -> (match rst with - | [|a;b|] when l = Lazy.force coq_and -> + | [|a;b|] when eq_constr l (Lazy.force coq_and) -> let f,env,tg = xparse_formula env tg a in let g,env, tg = xparse_formula env tg b in mkformula_binary mkC term f g,env,tg - | [|a;b|] when l = Lazy.force coq_or -> + | [|a;b|] when eq_constr l (Lazy.force coq_or) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkD term f g,env,tg - | [|a|] when l = Lazy.force coq_not -> + | [|a|] when eq_constr l (Lazy.force coq_not) -> let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when l = Lazy.force coq_iff -> + | [|a;b|] when eq_constr l (Lazy.force coq_iff) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg @@ -1126,8 +1126,8 @@ struct let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg - | _ when term = Lazy.force coq_True -> (TT,env,tg) - | _ when term = Lazy.force coq_False -> (FF,env,tg) + | _ when eq_constr term (Lazy.force coq_True) -> (TT,env,tg) + | _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg) | _ -> X(term),env,tg in xparse_formula env tg ((*Reductionops.whd_zeta*) term) -- cgit v1.2.3