From 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 26 Nov 2017 04:30:07 +0100 Subject: [api] Remove aliases of `Evar.t` There don't really bring anything, we also correct some minor nits with the printing function. --- proofs/evar_refiner.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/evar_refiner.mli') diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index a0e3b718a..d90cff572 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -14,5 +14,5 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr -val w_refine : evar * evar_info -> +val w_refine : Evar.t * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map -- cgit v1.2.3