summaryrefslogtreecommitdiff
path: root/toplevel/record.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.mli')
-rw-r--r--toplevel/record.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 8eff2ed5..66282c20 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: record.mli,v 1.16.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: record.mli 6743 2005-02-18 22:14:08Z herbelin $ i*)
(*i*)
open Names
@@ -21,7 +21,7 @@ open Topconstr
[coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> bool list -> rel_context -> constant option list
+ inductive -> bool list -> rel_context -> bool list * constant option list
val definition_structure :
lident with_coercion * local_binder list *