diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/cbn.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 0b13f4763a..bec9ede6f1 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -225,7 +225,7 @@ struct let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 | _, _ -> false in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a607c09010..f3ecc2a9f0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -540,7 +540,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> | (f, n, ar) :: oth -> let open Context.Named.Declaration in let (sp', u') = check_mutind env sigma n ar in - if not (MutInd.equal sp sp') then + if not (QMutInd.equal env sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" |