diff options
| author | letouzey | 2008-03-14 19:30:48 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-14 19:30:48 +0000 |
| commit | 9c699950feff3631c206f87f1d7d8c1686f1f597 (patch) | |
| tree | c6129e9db0e0760d3648730f4ac64320512be0df | |
| parent | dfb001fde305a4d3b4e418da39b4075cf55a7f57 (diff) | |
avoid universe problems with pf_get_type in f_equal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10670 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/cc/cctac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 8eda68e106..dc29e101aa 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -440,9 +440,9 @@ let congruence_tac depth l = let f_equal gl = let cut_eq c1 c2 = + let ty = refresh_universes (pf_type_of gl c1) in tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [| pf_type_of gl c1; c1; c2|]))) - reflexivity + (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) reflexivity in try match kind_of_term (pf_concl gl) with | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> |