summaryrefslogtreecommitdiff
path: root/pretyping/retyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/retyping.mli')
-rw-r--r--pretyping/retyping.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 923123c5..733cb4b1 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
+(*i $Id: retyping.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
(*i*)
open Names
@@ -34,5 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
(* Makes an unsafe judgment from a constr *)
val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
-val type_of_inductive_knowing_parameters : env -> evar_map -> inductive ->
+val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
constr array -> types
+