diff options
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index d023b4568..bcd31cb7e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -103,7 +103,7 @@ let get_coq_eq ctx = (Universes.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> - error "eq not found." + user_err Pp.(str "eq not found.") let univ_of_eq env eq = let eq = EConstr.of_constr eq in @@ -120,6 +120,8 @@ let univ_of_eq env eq = (* in which case, a symmetry lemma is definable *) (**********************************************************************) +let error msg = user_err Pp.(str msg) + let get_sym_eq_data env (ind,u) = let (mib,mip as specif) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || |