aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
authorppedrot2013-04-29 16:02:46 +0000
committerppedrot2013-04-29 16:02:46 +0000
commit943e6b23229b5eed2fb8265089563ce0a25b9b44 (patch)
tree803aa037f3413c21e76650c62e7ea9173ba3c918 /kernel/typeops.ml
parent4490dfcb94057dd6518963a904565e3a4a354bac (diff)
Merging Context and Sign.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r--kernel/typeops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a27ce1c479..cc7cf0c68a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -97,7 +97,7 @@ let judge_of_variable env id =
variables of the current env *)
(* TODO: check order? *)
let check_hyps_inclusion env c sign =
- Sign.fold_named_context
+ Context.fold_named_context
(fun (id,_,ty1) () ->
try
let ty2 = named_type id env in