diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 08:32:27 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 08:32:27 +0000 |
| commit | 2a20061cc2790eedee7fab6230fe1dd2b4d58c24 (patch) | |
| tree | 29cf49dbd60428709991f9d545b565751c03e858 /plugins/xml/doubleTypeInference.ml | |
| parent | ec5ed7870b4b59e05c5e994c9bad35e28685b8bd (diff) | |
Remove some uses of local modules (some were unused, some were costly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/doubleTypeInference.ml')
| -rw-r--r-- | plugins/xml/doubleTypeInference.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index 5a3880b01..d54308165 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -16,20 +16,17 @@ type types = {synthesized : Term.types ; expected : Term.types option};; let cprop = - let module N = Names in - N.make_con - (N.MPfile + Names.make_con + (Names.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.DirPath.empty) - (N.Label.make "CProp") + (Names.DirPath.empty) + (Names.Label.make "CProp") ;; let whd_betadeltaiotacprop env _evar_map ty = - let module C = Closure in - let module CR = C.RedFlags in (*** CProp is made Opaque ***) - let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in - C.whd_val (C.create_clos_infos flags env) (C.inject ty) + let flags = Closure.RedFlags.red_sub Closure.betadeltaiota (Closure.RedFlags.fCONST cprop) in + Closure.whd_val (Closure.create_clos_infos flags env) (Closure.inject ty) ;; |