From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sat, 13 Aug 2016 18:11:22 +0200 Subject: CLEANUP: minor readability improvements mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called. --- pretyping/coercion.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/coercion.ml') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f39..553786f58 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -153,7 +153,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env evdref x y in let dest_prod c = - let open Context.Rel.Declaration in match Reductionops.splay_prod_n env ( !evdref) 1 c with | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion -- cgit v1.2.3