From 611da26d847888031cac4d6976b9e7e1e90cdc0e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 9 Dec 2017 23:14:19 +0100 Subject: [api] Remove yet another type alias. --- proofs/refiner.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34e517aed..52dc8bfd8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) -- cgit v1.2.3