aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.mli
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-10-18 17:51:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-10-18 17:51:58 +0000
commitedfda2501f08f18e24bd2e3eca763eb1c2dec0ea (patch)
treee4c42c670c2f61b95a7a0f68fd96f635aeef8b2b /proofs/clenv.mli
parenta586cb418549eb523a3395155cab2560fd178571 (diff)
Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenv.mli')
-rw-r--r--proofs/clenv.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 353fe5198..aaf9637f8 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -80,7 +80,7 @@ val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
(* Exported for program.ml only *)
val clenv_add_sign :
- (identifier * typed_type) -> wc clausenv -> wc clausenv
+ (identifier * types) -> wc clausenv -> wc clausenv
val constrain_clenv_to_subterm :
wc clausenv -> constr * constr -> wc clausenv * constr
val clenv_constrain_dep_args_of :