From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 19 Apr 2011 16:44:20 +0200 Subject: Imported Upstream version 8.3.pl2 --- proofs/pfedit.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 1b284f8d..8df26706 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i*) (*i*) open Util @@ -202,6 +202,6 @@ val mutate : (pftreestate -> pftreestate) -> unit (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) -val build_constant_by_tactic : named_context_val -> types -> tactic -> +val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> Entries.definition_entry val build_by_tactic : types -> tactic -> constr -- cgit v1.2.3