diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:06 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:06 +0000 |
| commit | f9106194333c11ab86460660f3603565ecd7785a (patch) | |
| tree | 231c7a72af1f745f2a8588dcf9d49741dac672a9 /plugins/cc | |
| parent | 6039f99f7acd0d964449e9ed4e535cbd2796b87c (diff) | |
Fix congruence: normalise hypotheses with respect to evars.
Detected in CompCert.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 32e6d914f..a34cbf70f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -207,9 +207,9 @@ let make_prb gls depth additionnal_terms = neg_hyps:=(cid,nh):: !neg_hyps | `Rule patts -> add_quant state id true patts | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val (Goal.V82.hyps gls.sigma gls.it)); + end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); begin - match atom_of_constr env sigma (pf_concl gls) with + match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter |